diff --git a/arch/cortex-m/src/mpu.rs b/arch/cortex-m/src/mpu.rs
index 339a49522b..90000b199b 100644
--- a/arch/cortex-m/src/mpu.rs
+++ b/arch/cortex-m/src/mpu.rs
@@ -484,7 +484,8 @@ impl mpu::RegionDescriptor for CortexMRegion {
                     Self::start(p.fst),
                     Self::start(p.fst) + Self::size(p.fst) + Self::size(p.snd),
                     permissions
-                )
+                ) &&
+                valid_size(Self::start(p.fst) + Self::size(p.fst) + Self::size(p.snd))
             )
         }> requires valid_size(available_start + available_size) && max_region_number > 0 && max_region_number < 8
     )]
@@ -520,7 +521,7 @@ impl mpu::RegionDescriptor for CortexMRegion {
         // region size must be aligned to start
         start = align(start, region_size);
         // RJ: start = u32::MAX, region_size = u32::MAX/2 --> start + region_size overflows!
-         if start > overflow_bound {
+         if start > overflow_bound || size > (u32::MAX as usize) - start {
             // RJ: defensively adding check as otherwise `start + region_size` can overflow?
             return None;
         }
diff --git a/arch/cortex-m/src/tcb/theorems.rs b/arch/cortex-m/src/tcb/theorems.rs
index 0a12808c8a..1363e29c00 100644
--- a/arch/cortex-m/src/tcb/theorems.rs
+++ b/arch/cortex-m/src/tcb/theorems.rs
@@ -19,19 +19,19 @@ pub fn theorem_to_pow2_gt1(x: usize) {}
 #[flux_rs::sig(fn (usize[@n]) requires n < 32 ensures pow2(to_pow2(n)))]
 pub fn theorem_to_pow2_is_pow2(_n: usize) {}
 
-#[flux_rs::trusted(reason = "math")]
+#[flux_rs::proven_externally]
 #[flux_rs::sig(fn (usize[@x], usize[@y], usize[@z]) requires aligned(x, y) && z <= y && pow2(y) && pow2(z) ensures aligned(x, z))]
 pub fn theorem_pow2_le_aligned(x: usize, y: usize, z: usize) {}
 
-#[flux_rs::trusted(reason = "math")]
+#[flux_rs::proven_externally]
 #[flux_rs::sig(fn (r:usize) requires pow2(r) && r >= 8 ensures octet(r))]
 pub fn theorem_pow2_octet(_n: usize) {}
 
-#[flux_rs::trusted(reason = "math")]
+#[flux_rs::proven_externally]
 #[flux_rs::sig(fn (n:usize) requires pow2(n) && n >= 4 ensures pow2(n / 2))]
 pub fn theorem_pow2_div2_pow2(_n: usize) {}
 
-#[flux_rs::trusted(reason = "math")]
+#[flux_rs::proven_externally]
 #[flux_rs::sig(fn (n:usize) requires pow2(n) && n >= 2 ensures (n / 2) * 2 == n)]
 pub fn theorem_div2_pow2(_n: usize) {}
 
@@ -43,7 +43,7 @@ pub fn theorem_div_octet(_n: usize) {}
 #[flux_rs::sig(fn (x: usize, y: usize) requires aligned(x, y) ensures aligned(x + y, y))]
 pub fn theorem_aligned_plus_aligned_to_is_aligned(_x: usize, _y: usize) {}
 
-#[flux_rs::trusted(reason = "math")]
+#[flux_rs::proven_externally]
 #[flux_rs::sig(fn (x: usize, y: usize) requires y >= 32 && pow2(y) && aligned(x, y) ensures least_five_bits(bv32(x)) == 0)]
 pub fn theorem_aligned_value_ge32_lowest_five_bits0(x: usize, y: usize) {}
 
diff --git a/flux_support/src/flux_ptr.rs b/flux_support/src/flux_ptr.rs
index ec2af946ee..a1fce9d68c 100644
--- a/flux_support/src/flux_ptr.rs
+++ b/flux_support/src/flux_ptr.rs
@@ -157,7 +157,7 @@ impl FluxPtr {
         let n = self.as_usize();
         if offset <= u32::MAX as usize {
             // offset in bounds; test addition
-            n + offset <= (u32::MAX as usize)
+            n <= (u32::MAX as usize) - offset
         } else {
             // offset itself is out of bounds
             false
diff --git a/kernel/src/allocator.rs b/kernel/src/allocator.rs
index e29c280e23..e15c76a701 100644
--- a/kernel/src/allocator.rs
+++ b/kernel/src/allocator.rs
@@ -411,7 +411,8 @@ impl<R: RegionDescriptor + Display + Copy> AppMemoryAllocator<R> {
                     R::start(p.fst),
                     R::start(p.fst) + R::size(p.fst) + R::size(p.snd),
                     mpu::Permissions { r: true, w: true, x: false }
-                )
+                ) &&
+                valid_size(R::start(p.fst) + R::size(p.fst) + R::size(p.snd))
             )
         }, ()>
     )]
@@ -466,7 +467,11 @@ impl<R: RegionDescriptor + Display + Copy> AppMemoryAllocator<R> {
                 unallocated_memory_start + unallocated_memory_size <= u32::MAX &&
                 unallocated_memory_start > 0 &&
                 initial_kernel_memory_size > 0 &&
-                flash_start + flash_size < unallocated_memory_start
+                flash_start + flash_size < unallocated_memory_start &&
+                valid_size(R::start(ram_regions.fst) + R::size(ram_regions.fst) + initial_kernel_memory_size) &&
+                (R::is_set(ram_regions.snd) => (
+                    valid_size(initial_kernel_memory_size + R::start(ram_regions.fst) + R::size(ram_regions.fst) + R::size(ram_regions.snd))
+                ))
     )]
     fn get_app_breaks(
         ram_regions: Pair<R, R>,
@@ -578,10 +583,24 @@ impl<R: RegionDescriptor + Display + Copy> AppMemoryAllocator<R> {
         let Some(ram0_size) = ram_regions.fst.size() else {
             return Err(AllocateAppMemoryError::HeapError);
         };
+        let Some(ram0_start) = ram_regions.fst.start() else {
+            return Err(AllocateAppMemoryError::HeapError);
+        };
         if ram0_size > (u32::MAX as usize) - initial_kernel_memory_size {
             return Err(AllocateAppMemoryError::HeapError);
         }
 
+        if ram0_size + initial_kernel_memory_size
+                > (u32::MAX as usize) - ram0_start.as_usize() {
+                    return Err(AllocateAppMemoryError::HeapError);   
+                }
+        if ram_regions.snd.is_set()
+            && ram0_size + initial_kernel_memory_size
+                > (u32::MAX as usize) - ram_regions.snd.size().unwrap() - ram0_start.as_usize()
+        {
+            return Err(AllocateAppMemoryError::HeapError);
+        }
+
         // Get the app breaks using the RAM region
         let breaks = Self::get_app_breaks(
             ram_regions,
diff --git a/kernel/src/platform/mpu.rs b/kernel/src/platform/mpu.rs
index e973fc9d7d..cd9b8501a7 100644
--- a/kernel/src/platform/mpu.rs
+++ b/kernel/src/platform/mpu.rs
@@ -183,7 +183,8 @@ pub trait RegionDescriptor: core::marker::Sized {
                     Self::start(p.fst),
                     Self::start(p.fst) + Self::size(p.fst) + Self::size(p.snd),
                     permissions
-                )
+                ) &&
+                valid_size(Self::start(p.fst) + Self::size(p.fst) + Self::size(p.snd))
             )
         }> requires valid_size(available_start + available_size) && max_region_number > 0 && max_region_number < 8
     )]
@@ -387,7 +388,8 @@ impl RegionDescriptor for MpuRegionDefault {
                     Self::start(p.fst),
                     Self::start(p.fst) + Self::size(p.fst) + Self::size(p.snd),
                     permissions
-                )
+                ) &&
+                valid_size(Self::start(p.fst) + Self::size(p.fst) + Self::size(p.snd))
             )
         }> requires max_region_number > 0 && max_region_number < 8)]
     fn allocate_regions(
diff --git a/lean_proofs/.github/workflows/lean_action_ci.yml b/lean_proofs/.github/workflows/lean_action_ci.yml
new file mode 100644
index 0000000000..09cd4ca6df
--- /dev/null
+++ b/lean_proofs/.github/workflows/lean_action_ci.yml
@@ -0,0 +1,14 @@
+name: Lean Action CI
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+      - uses: leanprover/lean-action@v1
diff --git a/lean_proofs/.gitignore b/lean_proofs/.gitignore
new file mode 100644
index 0000000000..bfb30ec8c7
--- /dev/null
+++ b/lean_proofs/.gitignore
@@ -0,0 +1 @@
+/.lake
diff --git a/lean_proofs/LeanProofs.lean b/lean_proofs/LeanProofs.lean
new file mode 100644
index 0000000000..a5b5ef0d61
--- /dev/null
+++ b/lean_proofs/LeanProofs.lean
@@ -0,0 +1,3 @@
+-- This module serves as the root of the `LeanProofs` library.
+-- Import modules here that should be built as part of the library.
+import LeanProofs.Basic
diff --git a/lean_proofs/LeanProofs/Basic.lean b/lean_proofs/LeanProofs/Basic.lean
new file mode 100644
index 0000000000..99415d9d9f
--- /dev/null
+++ b/lean_proofs/LeanProofs/Basic.lean
@@ -0,0 +1 @@
+def hello := "world"
diff --git a/lean_proofs/LeanProofs/SharedLemmas.lean b/lean_proofs/LeanProofs/SharedLemmas.lean
new file mode 100644
index 0000000000..35cff7b46b
--- /dev/null
+++ b/lean_proofs/LeanProofs/SharedLemmas.lean
@@ -0,0 +1,143 @@
+namespace Nat
+
+def bit (b : Bool) : Nat → Nat := cond b (2 * · + 1) (2 * ·)
+
+theorem shiftRight_one (n) : n >>> 1 = n / 2 := rfl
+
+@[simp]
+theorem bit_decide_mod_two_eq_one_shiftRight_one (n : Nat) : bit (n % 2 = 1) (n >>> 1) = n := by
+  simp only [bit, shiftRight_one]
+  cases mod_two_eq_zero_or_one n with | _ h => simpa [h] using Nat.div_add_mod n 2
+
+theorem bit_testBit_zero_shiftRight_one (n : Nat) : bit (n.testBit 0) (n >>> 1) = n := by
+  simp
+
+/-- A recursion principle for `bit` representations of natural numbers.
+  For a predicate `motive : Nat → Sort u`, if instances can be
+  constructed for natural numbers of the form `bit b n`,
+  they can be constructed for all natural numbers. -/
+@[elab_as_elim, specialize]
+def binaryRec {motive : Nat → Sort u} (z : motive 0) (f : ∀ b n, motive n → motive (bit b n))
+    (n : Nat) : motive n :=
+  if n0 : n = 0 then congrArg motive n0 ▸ z
+  else
+    let x := f (1 &&& n != 0) (n >>> 1) (binaryRec z f (n >>> 1))
+    congrArg motive n.bit_testBit_zero_shiftRight_one ▸ x
+decreasing_by exact bitwise_rec_lemma n0
+
+end Nat
+
+theorem le_max_of_nat_eq_of_nat {w : Nat} (x y : Nat) :
+    x < 2 ^ w → y < 2 ^ w → (BitVec.ofNat w x = BitVec.ofNat w y ↔ x = y) := by
+  intros hx hy
+  apply Iff.intro
+  case mp =>
+    intro bv_eq
+    have fin_eq := congrArg BitVec.toFin bv_eq
+    simp [BitVec.toFin_ofNat, Fin.ofNat] at fin_eq
+    rw [Nat.mod_eq_of_lt, Nat.mod_eq_of_lt] at fin_eq
+    exact fin_eq
+    exact hy
+    exact hx
+  case mpr =>
+    intro eq
+    rw [eq]
+
+@[simp]
+def pow2 (n : Nat) : Bool :=
+  (n > 0) && ((n &&& (n - 1)) == 0)
+
+def i_pow2 (n : Int) : Bool :=
+  (let a3 := (BitVec.ofInt 32 n); ((n > 0) && ((BitVec.and a3 (BitVec.sub a3 1#32)) = 0#32)))
+
+theorem i_pow2_eq_pow2 (x: Nat) : (x < 2 ^ 32) -> (i_pow2 x <-> pow2 x) := by
+  unfold i_pow2 pow2
+  simp
+  intros x_in_bounds xgt0
+  apply Iff.intro
+  case mp =>
+    intros bv_eq
+    rw [
+      BitVec.ofNat_sub_ofNat_of_le,
+      ← BitVec.ofNat_and,
+      le_max_of_nat_eq_of_nat
+    ] at bv_eq
+    exact bv_eq
+    case _ =>
+      apply Nat.lt_of_le_of_lt
+      exact @Nat.and_le_right x (x - 1)
+      apply Nat.lt_trans (by omega : (x - 1) < x)
+      simp; exact x_in_bounds
+    case _ =>
+      simp
+    case _ =>
+      simp
+    case _ =>
+      exact xgt0
+  case mpr =>
+    intros bv_eq
+    rw [
+      BitVec.ofNat_sub_ofNat_of_le,
+      ← BitVec.ofNat_and,
+      le_max_of_nat_eq_of_nat
+    ]
+    exact bv_eq
+    case _ =>
+      apply Nat.lt_of_le_of_lt
+      exact @Nat.and_le_right x (x - 1)
+      apply Nat.lt_trans (by omega : (x - 1) < x)
+      simp; exact x_in_bounds
+    case _ => simp
+    case _ => simp
+    case _ => exact xgt0
+
+theorem fold_land : (Nat.bitwise and x x) = x &&& x := by rfl
+
+theorem pow2_isPowerOfTwo (x : Nat) : pow2 x <-> x.isPowerOfTwo := by
+  apply Iff.intro
+  case mp =>
+    intro h
+    induction x using Nat.binaryRec
+    case z => simp_all!
+    case f b n ih =>
+      simp_all [Nat.bit]
+      cases b
+      · simp_all!
+        rcases h with ⟨_, h⟩
+        rw [Nat.mul_comm]
+        apply Nat.isPowerOfTwo_mul_two_of_isPowerOfTwo
+        apply ih
+        simp_all [HAnd.hAnd, AndOp.and, Nat.land]
+        unfold Nat.bitwise at h
+        split at h ; omega
+        split at h ; omega
+        simp_all
+        have p : (2 * n - 1) /2 = n - 1 := by cases n ; trivial ; simp +arith [Nat.left_distrib, Nat.mul_add_div]
+        simp_all
+      · simp_all
+        simp [HAnd.hAnd, AndOp.and, Nat.land] at h
+        unfold Nat.bitwise at h
+        split at h ; simp_all
+        split at h ; simp_all ; exists 0
+        simp_all [Nat.mul_add_div, fold_land]
+  case mpr =>
+    intro h
+    rcases h with ⟨n, h⟩
+    simp
+    and_intros
+    · simp_all ; apply Nat.pow_pos ; simp
+    · induction n generalizing x <;> simp_all
+
+theorem i_pow2_0_is_power_of_2 (x: Nat) : (x < 2 ^ 32) -> (i_pow2 x <-> x.isPowerOfTwo) := by
+  intro x_in_bounds
+  apply Iff.intro
+  case _ =>
+    intro x_pow2
+    rw [← pow2_isPowerOfTwo x]
+    apply (i_pow2_eq_pow2 x x_in_bounds).mp
+    exact x_pow2
+  case _ =>
+    intro x_pow2
+    apply (i_pow2_eq_pow2 x x_in_bounds).mpr
+    rw [pow2_isPowerOfTwo]
+    exact x_pow2
diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0.lean
new file mode 100644
index 0000000000..214f9521ca
--- /dev/null
+++ b/lean_proofs/LeanProofs/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0.lean
@@ -0,0 +1,11 @@
+-- GENERATED; DO NOT EDIT --
+-- FUNCTIONS --
+def f_aligned_1 (a2 : Int) (a3 : Int) : Bool :=
+  ((a2 % a3) = 0)
+
+def f_pow2_0 (a0 : Int) : Bool :=
+  (let a1 := (BitVec.ofInt 32 a0); ((a0 > 0) && ((BitVec.and a1 (BitVec.sub a1 1#32)) = 0#32)))
+
+-- THEOREM --
+def tcb_theorems_theorem_aligned_value_ge32_lowest_five_bits0 : Prop := (∀ (reftgen_x_0 : Int), (∀ (reftgen_y_1 : Int), (∀ (__ : Int), (((reftgen_y_1 ≥ 32) ∧ (f_pow2_0 reftgen_y_1) ∧ (f_aligned_1 reftgen_x_0 reftgen_y_1)) -> (∀ (__ : Int), ((reftgen_x_0 ≥ 0) -> (∀ (__ : Int), ((reftgen_x_0 ≤ 4294967295) -> (∀ (__ : Int), ((reftgen_y_1 ≥ 0) -> (∀ (__ : Int), ((reftgen_y_1 ≤ 4294967295) -> ((BitVec.and (BitVec.ofInt 32 reftgen_x_0) 31#32) = 0#32)))))))))))))
+
diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0Proof.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0Proof.lean
new file mode 100644
index 0000000000..27d9ebd61d
--- /dev/null
+++ b/lean_proofs/LeanProofs/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0Proof.lean
@@ -0,0 +1,37 @@
+import LeanProofs.TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0
+import LeanProofs.SharedLemmas
+import Init.Data.BitVec.Lemmas
+
+
+theorem f_pow2_0_eq_i_pow2 : f_pow2_0 = i_pow2 := by
+  funext x ; unfold f_pow2_0 i_pow2 ; simp
+
+def tcb_theorems_theorem_aligned_value_ge32_lowest_five_bits0_proof : tcb_theorems_theorem_aligned_value_ge32_lowest_five_bits0 := by
+  unfold tcb_theorems_theorem_aligned_value_ge32_lowest_five_bits0
+  intro x y _ h _ x_ge0 _ x_in_bounds _ y_ge0 _ y_in_bounds
+  obtain ⟨y_ge32, y_pow2, x_aligned_y⟩ := h
+  rw [f_pow2_0_eq_i_pow2] at *
+  unfold f_aligned_1 at x_aligned_y; simp at x_aligned_y
+  rw [
+    ← Int.toNat_of_nonneg x_ge0,
+    BitVec.ofInt_natCast,
+    BitVec.and_eq,
+    ←BitVec.ofNat_and
+  ]
+  simp [Nat.and_two_pow_sub_one_eq_mod _ 5]
+  have xnat_aligned_ynat : x.toNat % y.toNat = 0 := by
+    rw [← Int.toNat_emod x_ge0 y_ge0, x_aligned_y]
+    simp
+  rw [← Int.toNat_of_nonneg y_ge0] at y_pow2
+  have ynat_pow2 := (i_pow2_0_is_power_of_2 y.toNat (by omega)).mp y_pow2
+  rcases ynat_pow2 with ⟨k, hk⟩
+  rw [hk] at xnat_aligned_ynat
+  have ynat_dvd_xnat := Nat.dvd_of_mod_eq_zero xnat_aligned_ynat
+  have thirty_two_dvd_x : 32 ∣ x.toNat := by
+    apply @Nat.pow_dvd_of_le_of_pow_dvd 2 5 k
+    · apply (@Nat.pow_le_pow_iff_right 2 5 k (by omega)).mp
+      rw [← hk]
+      omega
+    · assumption
+  have x_mod_32_eq_0 := Nat.mod_eq_zero_of_dvd thirty_two_dvd_x
+  rw [x_mod_32_eq_0]
diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremDiv2Pow2.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremDiv2Pow2.lean
new file mode 100644
index 0000000000..09d4386ce8
--- /dev/null
+++ b/lean_proofs/LeanProofs/TcbTheoremsTheoremDiv2Pow2.lean
@@ -0,0 +1,8 @@
+-- GENERATED; DO NOT EDIT --
+-- FUNCTIONS --
+def f_pow2_0 (a0 : Int) : Bool :=
+  (let a1 := (BitVec.ofInt 32 a0); ((a0 > 0) && ((BitVec.and a1 (BitVec.sub a1 1#32)) = 0#32)))
+
+-- THEOREM --
+def tcb_theorems_theorem_div2_pow2 : Prop := (∀ (reftgen_n_0 : Int), (∀ (__ : Int), (((f_pow2_0 reftgen_n_0) ∧ (reftgen_n_0 ≥ 2)) -> (∀ (__ : Int), ((reftgen_n_0 ≥ 0) -> (∀ (__ : Int), ((reftgen_n_0 ≤ 4294967295) -> (((reftgen_n_0 / 2) * 2) = reftgen_n_0))))))))
+
diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremDiv2Pow2Proof.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremDiv2Pow2Proof.lean
new file mode 100644
index 0000000000..6d0005462c
--- /dev/null
+++ b/lean_proofs/LeanProofs/TcbTheoremsTheoremDiv2Pow2Proof.lean
@@ -0,0 +1,20 @@
+import LeanProofs.TcbTheoremsTheoremDiv2Pow2
+import LeanProofs.SharedLemmas
+
+theorem f_pow2_0_eq_i_pow2 : f_pow2_0 = i_pow2 := by
+  funext x; unfold f_pow2_0 i_pow2; simp
+
+def tcb_theorems_theorem_div2_pow2_proof : tcb_theorems_theorem_div2_pow2 := by
+  unfold tcb_theorems_theorem_div2_pow2
+  intro n _ h _ n_ge0 _ n_in_bounds
+  obtain ⟨n_pow2, n_ge2⟩ := h
+  rw [f_pow2_0_eq_i_pow2] at *
+  have res_nat : (n.toNat / 2) * 2 = n.toNat := by
+    rw [Nat.div_mul_cancel]
+    rw [←Int.toNat_of_nonneg n_ge0] at n_pow2
+    have nnat_pow2 := (i_pow2_0_is_power_of_2 n.toNat (by omega)).mp n_pow2
+    rcases nnat_pow2 with ⟨k, hy⟩
+    cases k with
+    | zero => omega
+    | succ k' => omega
+  omega
diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Div2Pow2.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Div2Pow2.lean
new file mode 100644
index 0000000000..d1421ac0a0
--- /dev/null
+++ b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Div2Pow2.lean
@@ -0,0 +1,8 @@
+-- GENERATED; DO NOT EDIT --
+-- FUNCTIONS --
+def f_pow2_0 (a0 : Int) : Bool :=
+  (let a1 := (BitVec.ofInt 32 a0); ((a0 > 0) && ((BitVec.and a1 (BitVec.sub a1 1#32)) = 0#32)))
+
+-- THEOREM --
+def tcb_theorems_theorem_pow2_div2_pow2 : Prop := (∀ (reftgen_n_0 : Int), (∀ (__ : Int), (((f_pow2_0 reftgen_n_0) ∧ (reftgen_n_0 ≥ 4)) -> (∀ (__ : Int), ((reftgen_n_0 ≥ 0) -> (∀ (__ : Int), ((reftgen_n_0 ≤ 4294967295) -> (f_pow2_0 (reftgen_n_0 / 2)))))))))
+
diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Div2Pow2Proof.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Div2Pow2Proof.lean
new file mode 100644
index 0000000000..a8b613e66e
--- /dev/null
+++ b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Div2Pow2Proof.lean
@@ -0,0 +1,51 @@
+import LeanProofs.TcbTheoremsTheoremPow2Div2Pow2
+import LeanProofs.SharedLemmas
+
+theorem f_pow2_eq_i_pow2 : f_pow2_0 = i_pow2 := by
+  funext x; unfold f_pow2_0 i_pow2; simp
+
+theorem pow_right_inj (ha : 1 < a) : a ^ m = a ^ n ↔ m = n := by
+  simp [Nat.le_antisymm_iff, Nat.pow_le_pow_iff_right ha]
+
+theorem four_is_pow2 : pow2 4 := by simp
+
+theorem pow2_div2_pow2 (x : Nat) : pow2 x -> x >= 4 -> pow2 (x / 2) := by
+  intros h1 h2
+  rcases (pow2_isPowerOfTwo x).mp h1 with ⟨n, hy⟩
+  rcases (pow2_isPowerOfTwo 4).mp four_is_pow2 with ⟨m, hz⟩
+  apply (pow2_isPowerOfTwo (x / 2)).mpr
+  simp_all
+  simp [Nat.isPowerOfTwo]
+  exists (n - 1)
+  have hn: n ≥ 1 := by
+    simp_all [Nat.pow_le_pow_iff_right]
+    have h_eq : 2 ^ 2 = 2 ^ m := by rw [← hz]
+    have hm: m = 2 := by
+      rw [pow_right_inj] at h_eq ; simp_all ; omega
+    simp_all; omega
+  rw [Nat.div_eq_iff_eq_mul_left]
+  rw [<- Nat.pow_pred_mul] <;> omega
+  omega
+  have h3 : (2 ∣ 2 ^ n) = (2 ^ 1 ∣ 2 ^ n) := by simp
+  simp [h3]
+  apply Nat.pow_dvd_pow <;> omega
+
+
+def tcb_theorems_theorem_pow2_div2_pow2_proof : tcb_theorems_theorem_pow2_div2_pow2 := by
+  unfold tcb_theorems_theorem_pow2_div2_pow2
+  intro n _ h _ n_ge0 _ n_in_bounds
+  obtain ⟨n_pow2, n_ge4⟩ := h
+  rw [f_pow2_eq_i_pow2] at *
+  have ntwo_in_bounds: (n.toNat / 2) < 2 ^ 32 := by omega
+  have nnat_in_bounds: n.toNat < 2 ^ 32 := by omega
+  have res_n: f_pow2_0 (n.toNat / 2) = true := by
+    apply (i_pow2_eq_pow2 (n.toNat / 2) ntwo_in_bounds).mpr
+    apply pow2_div2_pow2
+    apply (i_pow2_eq_pow2 n.toNat nnat_in_bounds).mp
+    rw [Int.toNat_of_nonneg]
+    assumption
+    assumption
+    omega
+  rw [Int.toNat_of_nonneg] at res_n
+  assumption
+  assumption
diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2LeAligned.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2LeAligned.lean
new file mode 100644
index 0000000000..c333f67c41
--- /dev/null
+++ b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2LeAligned.lean
@@ -0,0 +1,11 @@
+-- GENERATED; DO NOT EDIT --
+-- FUNCTIONS --
+def f_aligned_0 (a0 : Int) (a1 : Int) : Bool :=
+  ((a0 % a1) = 0)
+
+def f_pow2_1 (a2 : Int) : Bool :=
+  (let a3 := (BitVec.ofInt 32 a2); ((a2 > 0) && ((BitVec.and a3 (BitVec.sub a3 1#32)) = 0#32)))
+
+-- THEOREM --
+def tcb_theorems_theorem_pow2_le_aligned : Prop := (∀ (reftgen_x_0 : Int), (∀ (reftgen_y_1 : Int), (∀ (reftgen_z_2 : Int), (∀ (__ : Int), (((f_aligned_0 reftgen_x_0 reftgen_y_1) ∧ (reftgen_z_2 ≤ reftgen_y_1) ∧ (f_pow2_1 reftgen_y_1) ∧ (f_pow2_1 reftgen_z_2)) -> (∀ (__ : Int), ((reftgen_x_0 ≥ 0) -> (∀ (__ : Int), ((reftgen_x_0 ≤ 4294967295) -> (∀ (__ : Int), ((reftgen_y_1 ≥ 0) -> (∀ (__ : Int), ((reftgen_y_1 ≤ 4294967295) -> (∀ (__ : Int), ((reftgen_z_2 ≥ 0) -> (∀ (__ : Int), ((reftgen_z_2 ≤ 4294967295) -> (f_aligned_0 reftgen_x_0 reftgen_z_2))))))))))))))))))
+
diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2LeAlignedProof.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2LeAlignedProof.lean
new file mode 100644
index 0000000000..8b0318c2c1
--- /dev/null
+++ b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2LeAlignedProof.lean
@@ -0,0 +1,57 @@
+import LeanProofs.TcbTheoremsTheoremPow2LeAligned
+import LeanProofs.SharedLemmas
+
+theorem f_pow2_1_eq_i_pow2 : f_pow2_1 = i_pow2 := by
+  funext x; unfold f_pow2_1 i_pow2; simp
+
+theorem mod_pow2_le {x n m : Nat} : m <= n -> x % 2 ^ n = 0 -> x % 2 ^ m = 0 := by
+  intros h1 h2
+  simp_all [Nat.mod_eq_iff]
+  rcases h2 with ⟨a, ⟨k, _⟩⟩
+  case _ =>
+    apply And.intro
+    · apply Nat.pow_pos ; simp
+    · exists (2 ^ (n - m) * k)
+      conv => right ; rw [←Nat.mul_assoc] ; left ; rw [Nat.mul_comm, Nat.pow_sub_mul_pow 2 h1]
+      assumption
+
+theorem pow2_le_aligned (x y z : Nat) :
+  x % y = 0 ->
+  z <= y ->
+  pow2 y ->
+  pow2 z ->
+  x % z = 0 :=
+by
+  intros h1 h2 h3 h4
+  rcases (pow2_isPowerOfTwo y).mp h3 with ⟨n, hy⟩
+  rcases (pow2_isPowerOfTwo z).mp h4 with ⟨m, hz⟩
+  simp_all
+  have h := (Nat.pow_le_pow_iff_right (a := 2) (by simp)).mp h2
+  apply mod_pow2_le h
+  assumption
+
+def tcb_theorems_theorem_pow2_le_aligned_proof : tcb_theorems_theorem_pow2_le_aligned := by
+  unfold tcb_theorems_theorem_pow2_le_aligned
+  intros x y z _ h _ x_ge0 _ x_in_bounds _ y_ge0 _ y_in_bounds _ z_ge0 _ z_in_bounds
+  obtain ⟨x_aligned_y, ⟨z_le_y, ⟨y_pow2, z_pow2⟩⟩⟩ := h
+  rw [f_pow2_1_eq_i_pow2] at *
+  unfold f_aligned_0 at *
+  simp at x_aligned_y
+  simp
+  have nat_res : x.toNat % z.toNat = 0 := by
+    apply pow2_le_aligned x.toNat y.toNat z.toNat
+    · rw [←Int.toNat_of_nonneg x_ge0, ←Int.toNat_of_nonneg y_ge0] at x_aligned_y
+      omega
+    · omega
+    · apply (i_pow2_eq_pow2 y.toNat _).mp
+      rw [Int.toNat_of_nonneg]
+      assumption
+      assumption
+      omega
+    · apply (i_pow2_eq_pow2 z.toNat _).mp
+      rw [Int.toNat_of_nonneg]
+      assumption
+      assumption
+      omega
+  rw [←Int.toNat_of_nonneg x_ge0, ←Int.toNat_of_nonneg z_ge0]
+  omega
diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Octet.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Octet.lean
new file mode 100644
index 0000000000..8546d24636
--- /dev/null
+++ b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Octet.lean
@@ -0,0 +1,11 @@
+-- GENERATED; DO NOT EDIT --
+-- FUNCTIONS --
+def f_octet_1 (a2 : Int) : Bool :=
+  ((a2 % 8) = 0)
+
+def f_pow2_0 (a0 : Int) : Bool :=
+  (let a1 := (BitVec.ofInt 32 a0); ((a0 > 0) && ((BitVec.and a1 (BitVec.sub a1 1#32)) = 0#32)))
+
+-- THEOREM --
+def tcb_theorems_theorem_pow2_octet : Prop := (∀ (reftgen_r_0 : Int), (∀ (__ : Int), (((f_pow2_0 reftgen_r_0) ∧ (reftgen_r_0 ≥ 8)) -> (∀ (__ : Int), ((reftgen_r_0 ≥ 0) -> (∀ (__ : Int), ((reftgen_r_0 ≤ 4294967295) -> (f_octet_1 reftgen_r_0))))))))
+
diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2OctetProof.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2OctetProof.lean
new file mode 100644
index 0000000000..8fd6d21ff1
--- /dev/null
+++ b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2OctetProof.lean
@@ -0,0 +1,41 @@
+import LeanProofs.TcbTheoremsTheoremPow2Octet
+import LeanProofs.SharedLemmas
+
+theorem f_pow2_1_eq_i_pow2 : f_pow2_0 = i_pow2 := by
+  funext x; unfold f_pow2_0 i_pow2; simp
+
+theorem power_of_2_ge_8_octet (x: Nat) : x.isPowerOfTwo -> x ≥ 8 -> x % 8 = 0 := by
+  intro x_pow2 x_ge8
+  apply Nat.mod_eq_zero_of_dvd
+  unfold Nat.isPowerOfTwo at x_pow2
+  cases x_pow2 with
+  | intro k hk =>
+    have h : (8 = 2 ^ 3) := by simp
+    rw [hk, h,  Nat.pow_dvd_pow_iff_le_right]
+    case _ =>
+      rw [hk, h] at x_ge8
+      rw [←(@Nat.pow_le_pow_iff_right 2 3 k)]
+      exact x_ge8
+      simp
+    case _ => simp
+
+def tcb_theorems_theorem_pow2_octet_proof : tcb_theorems_theorem_pow2_octet := by
+  unfold tcb_theorems_theorem_pow2_octet
+  intro r0 _ h1 _ r0_ge0 _ r0_in_bounds
+  obtain ⟨r0_pow2, r0_ge8⟩ := h1
+  rw [f_pow2_1_eq_i_pow2] at *
+  unfold f_octet_1
+  simp
+  have nat_res : r0.toNat % 8 = 0 := by
+    apply power_of_2_ge_8_octet
+    case _ =>
+      apply (i_pow2_0_is_power_of_2 r0.toNat _).mp
+      case _ =>
+        rw [Int.toNat_of_nonneg]
+        assumption
+        assumption
+      case _ =>
+        omega
+    case _ =>
+      omega
+  omega
diff --git a/lean_proofs/README.md b/lean_proofs/README.md
new file mode 100644
index 0000000000..b8429d6ecb
--- /dev/null
+++ b/lean_proofs/README.md
@@ -0,0 +1 @@
+# lean_proofs
\ No newline at end of file
diff --git a/lean_proofs/lake-manifest.json b/lean_proofs/lake-manifest.json
new file mode 100644
index 0000000000..49f8bbbb47
--- /dev/null
+++ b/lean_proofs/lake-manifest.json
@@ -0,0 +1,5 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "lean_proofs",
+ "lakeDir": ".lake"}
diff --git a/lean_proofs/lakefile.toml b/lean_proofs/lakefile.toml
new file mode 100644
index 0000000000..4fe9f7cc84
--- /dev/null
+++ b/lean_proofs/lakefile.toml
@@ -0,0 +1,6 @@
+name = "lean_proofs"
+version = "0.1.0"
+defaultTargets = ["LeanProofs"]
+
+[[lean_lib]]
+name = "LeanProofs"
diff --git a/lean_proofs/lean-toolchain b/lean_proofs/lean-toolchain
new file mode 100644
index 0000000000..7f254a98f3
--- /dev/null
+++ b/lean_proofs/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.23.0