diff --git a/crates/domain/src/lib.rs b/crates/domain/src/lib.rs
index 47e94a2..91866fb 100644
--- a/crates/domain/src/lib.rs
+++ b/crates/domain/src/lib.rs
@@ -1,5 +1,8 @@
 #![no_std]
 
+#[cfg(kani)]
+pub mod proofs;
+
 pub mod capability;
 pub mod endpoint;
 pub mod error;
diff --git a/crates/domain/src/proofs.rs b/crates/domain/src/proofs.rs
new file mode 100644
index 0000000..dec8cc3
--- /dev/null
+++ b/crates/domain/src/proofs.rs
@@ -0,0 +1,184 @@
+#[cfg(kani)]
+mod kani_proofs {
+    use crate::capability::{Capability, CapabilityTable};
+    use crate::resource::Resource;
+    use crate::thread::{BlockReason, Thread, ThreadState};
+    use types::bounded::{CapSlot, Priority};
+    use types::generation::Generation;
+    use types::id::{CoreId, EndpointId, ProcessId, ThreadId};
+    use types::permission::{Permission, PermissionSet};
+    use types::time::TimeSlice;
+
+    // --- Capability non-escalation ---
+
+    #[kani::proof]
+    fn delegation_via_cap_table_never_escalates() {
+        let source_bits: u8 = kani::any();
+        let restrict_bits: u8 = kani::any();
+        let ep_id: u16 = kani::any();
+        kani::assume(ep_id < 256);
+
+        let source_perms = PermissionSet::from_bits(source_bits);
+        kani::assume(source_perms.allows(Permission::Delegate));
+
+        let resource = Resource::Endpoint(EndpointId::from_raw(ep_id));
+        let source_cap = Capability::new(resource.clone(), source_perms, Generation::initial());
+
+        let mut source_table = CapabilityTable::new();
+        let slot = source_table.insert(source_cap);
+        kani::assume(slot.is_ok());
+        let slot = slot.unwrap();
+
+        let cap = source_table.get(slot).unwrap();
+        let original_perms = *cap.permissions();
+        let delegated_perms = original_perms.restrict_to(&PermissionSet::from_bits(restrict_bits));
+
+        let mut target_table = CapabilityTable::new();
+        let delegated_cap = Capability::new(cap.resource().clone(), delegated_perms, Generation::initial());
+        let target_slot = target_table.insert(delegated_cap);
+        kani::assume(target_slot.is_ok());
+
+        let result = target_table.get(target_slot.unwrap()).unwrap();
+        assert!(result.permissions().is_subset_of(&original_perms));
+    }
+
+    #[kani::proof]
+    fn delegation_cannot_add_permissions_not_in_source() {
+        let source_bits: u8 = kani::any();
+        let restrict_bits: u8 = kani::any();
+
+        let source = PermissionSet::from_bits(source_bits);
+        let restrict = PermissionSet::from_bits(restrict_bits);
+        let result = source.restrict_to(&restrict);
+
+        if !source.allows(Permission::Read) {
+            assert!(!result.allows(Permission::Read));
+        }
+        if !source.allows(Permission::Write) {
+            assert!(!result.allows(Permission::Write));
+        }
+        if !source.allows(Permission::Execute) {
+            assert!(!result.allows(Permission::Execute));
+        }
+        if !source.allows(Permission::Delegate) {
+            assert!(!result.allows(Permission::Delegate));
+        }
+        if !source.allows(Permission::Revoke) {
+            assert!(!result.allows(Permission::Revoke));
+        }
+    }
+
+    // --- Capability table integrity ---
+
+    #[kani::proof]
+    fn cap_table_insert_get_roundtrip() {
+        let bits: u8 = kani::any();
+        let ep_id: u16 = kani::any();
+        kani::assume(ep_id < 256);
+
+        let perms = PermissionSet::from_bits(bits);
+        let resource = Resource::Endpoint(EndpointId::from_raw(ep_id));
+        let cap = Capability::new(resource, perms, Generation::initial());
+
+        let mut table = CapabilityTable::new();
+        let slot = table.insert(cap);
+        kani::assume(slot.is_ok());
+        let slot = slot.unwrap();
+
+        let retrieved = table.get(slot).unwrap();
+        assert!(*retrieved.permissions() == perms);
+    }
+
+    #[kani::proof]
+    fn cap_table_remove_then_get_fails() {
+        let bits: u8 = kani::any();
+
+        let cap = Capability::new(
+            Resource::ProcessCreate,
+            PermissionSet::from_bits(bits),
+            Generation::initial(),
+        );
+
+        let mut table = CapabilityTable::new();
+        let slot = table.insert(cap);
+        kani::assume(slot.is_ok());
+        let slot = slot.unwrap();
+
+        table.remove(slot).unwrap();
+        assert!(table.get(slot).is_err());
+    }
+
+    // --- Thread state machine safety ---
+
+    #[kani::proof]
+    fn dead_thread_rejects_all_transitions() {
+        let mut thread = Thread::new(
+            ThreadId::from_raw(0),
+            ProcessId::from_raw(0),
+            Priority::new(16).unwrap(),
+            TimeSlice::new(100),
+            None,
+        );
+
+        thread.set_running(CoreId::from_raw(0)).unwrap();
+        thread.exit().unwrap();
+
+        assert!(matches!(thread.state(), ThreadState::Dead));
+        assert!(thread.set_running(CoreId::from_raw(0)).is_err());
+        assert!(thread.block(BlockReason::WaitingAny).is_err());
+        assert!(thread.unblock().is_err());
+        assert!(thread.preempt().is_err());
+        assert!(thread.exit().is_err());
+    }
+
+    #[kani::proof]
+    fn only_running_thread_can_block() {
+        let prio_val: u8 = kani::any();
+        kani::assume(prio_val <= 31);
+        let prio = Priority::new(prio_val).unwrap();
+
+        let thread = Thread::new(
+            ThreadId::from_raw(0),
+            ProcessId::from_raw(0),
+            prio,
+            TimeSlice::new(100),
+            None,
+        );
+
+        assert!(matches!(thread.state(), ThreadState::Ready));
+        assert!(thread.block(BlockReason::WaitingAny).is_err());
+    }
+
+    #[kani::proof]
+    fn blocked_thread_cannot_run_directly() {
+        let mut thread = Thread::new(
+            ThreadId::from_raw(0),
+            ProcessId::from_raw(0),
+            Priority::new(16).unwrap(),
+            TimeSlice::new(100),
+            None,
+        );
+
+        thread.set_running(CoreId::from_raw(0)).unwrap();
+        thread.block(BlockReason::WaitingAny).unwrap();
+
+        assert!(thread.set_running(CoreId::from_raw(0)).is_err());
+    }
+
+    // --- Chained delegation ---
+
+    #[kani::proof]
+    fn chained_delegation_never_escalates() {
+        let original_bits: u8 = kani::any();
+        let restrict1_bits: u8 = kani::any();
+        let restrict2_bits: u8 = kani::any();
+
+        let original = PermissionSet::from_bits(original_bits);
+        let after_first = original.restrict_to(&PermissionSet::from_bits(restrict1_bits));
+        let after_second = after_first.restrict_to(&PermissionSet::from_bits(restrict2_bits));
+
+        assert!(after_first.is_subset_of(&original));
+        assert!(after_second.is_subset_of(&after_first));
+        assert!(after_second.is_subset_of(&original));
+    }
+}
diff --git a/crates/kernel/src/lib.rs b/crates/kernel/src/lib.rs
index dcbcfa0..a5d1b2e 100644
--- a/crates/kernel/src/lib.rs
+++ b/crates/kernel/src/lib.rs
@@ -1,6 +1,8 @@
 #![no_std]
 
 pub mod interrupt;
+#[cfg(kani)]
+pub mod proofs;
 pub mod syscall;
 
 pub use syscall::{SyscallOutcome, SyscallResult};
diff --git a/crates/kernel/src/proofs.rs b/crates/kernel/src/proofs.rs
new file mode 100644
index 0000000..3982827
--- /dev/null
+++ b/crates/kernel/src/proofs.rs
@@ -0,0 +1,142 @@
+#[cfg(kani)]
+mod kani_proofs {
+    use domain::capability::{Capability, CapabilityTable};
+    use domain::resource::Resource;
+    use types::bounded::CapSlot;
+    use types::generation::Generation;
+    use types::id::{EndpointId, ProcessId};
+    use types::permission::{Permission, PermissionSet};
+
+    #[kani::proof]
+    fn kernel_delegate_path_never_escalates() {
+        let source_bits: u8 = kani::any();
+        let restrict_bits: u8 = kani::any();
+        let ep_id: u16 = kani::any();
+        kani::assume(ep_id < 256);
+
+        let source_perms = PermissionSet::from_bits(source_bits);
+        kani::assume(source_perms.allows(Permission::Delegate));
+
+        let resource = Resource::Endpoint(EndpointId::from_raw(ep_id));
+
+        // Step 1: source process has a capability (simulates check_cap)
+        let mut source_table = CapabilityTable::new();
+        let source_cap = Capability::new(resource.clone(), source_perms, Generation::initial());
+        let slot = source_table.insert(source_cap);
+        kani::assume(slot.is_ok());
+        let slot = slot.unwrap();
+
+        // Step 2: kernel reads source cap and restricts (simulates handle_delegate)
+        let cap = source_table.get(slot).unwrap();
+        let original_perms = *cap.permissions();
+        let restricted = original_perms.restrict_to(&PermissionSet::from_bits(restrict_bits));
+
+        // Step 3: kernel inserts into target (simulates grant_cap)
+        let mut target_table = CapabilityTable::new();
+        let delegated = Capability::new(cap.resource().clone(), restricted, Generation::initial());
+        let target_slot = target_table.insert(delegated);
+        kani::assume(target_slot.is_ok());
+
+        // PROOF: the capability in the target table has permissions
+        // that are a strict subset of what the source held
+        let result = target_table.get(target_slot.unwrap()).unwrap();
+        assert!(result.permissions().is_subset_of(&original_perms));
+
+        // PROOF: no individual permission was gained
+        if !original_perms.allows(Permission::Read) {
+            assert!(!result.permissions().allows(Permission::Read));
+        }
+        if !original_perms.allows(Permission::Write) {
+            assert!(!result.permissions().allows(Permission::Write));
+        }
+        if !original_perms.allows(Permission::Execute) {
+            assert!(!result.permissions().allows(Permission::Execute));
+        }
+        if !original_perms.allows(Permission::Delegate) {
+            assert!(!result.permissions().allows(Permission::Delegate));
+        }
+        if !original_perms.allows(Permission::Revoke) {
+            assert!(!result.permissions().allows(Permission::Revoke));
+        }
+    }
+
+    #[kani::proof]
+    fn kernel_chained_delegate_never_escalates() {
+        let original_bits: u8 = kani::any();
+        let restrict1_bits: u8 = kani::any();
+        let restrict2_bits: u8 = kani::any();
+        let ep_id: u16 = kani::any();
+        kani::assume(ep_id < 256);
+
+        let original_perms = PermissionSet::from_bits(original_bits);
+        kani::assume(original_perms.allows(Permission::Delegate));
+
+        let resource = Resource::Endpoint(EndpointId::from_raw(ep_id));
+
+        // Process A has the original cap
+        let mut table_a = CapabilityTable::new();
+        let cap_a = Capability::new(resource.clone(), original_perms, Generation::initial());
+        let slot_a = table_a.insert(cap_a);
+        kani::assume(slot_a.is_ok());
+        let slot_a = slot_a.unwrap();
+
+        // A delegates to B
+        let cap = table_a.get(slot_a).unwrap();
+        let perms_for_b = cap.permissions().restrict_to(&PermissionSet::from_bits(restrict1_bits));
+        let mut table_b = CapabilityTable::new();
+        let cap_b = Capability::new(resource.clone(), perms_for_b, Generation::initial());
+        let slot_b = table_b.insert(cap_b);
+        kani::assume(slot_b.is_ok());
+        let slot_b = slot_b.unwrap();
+
+        // B delegates to C (if B has Delegate permission)
+        let cap_in_b = table_b.get(slot_b).unwrap();
+        if cap_in_b.permissions().allows(Permission::Delegate) {
+            let perms_for_c = cap_in_b.permissions().restrict_to(&PermissionSet::from_bits(restrict2_bits));
+            let mut table_c = CapabilityTable::new();
+            let cap_c = Capability::new(resource, perms_for_c, Generation::initial());
+            let slot_c = table_c.insert(cap_c);
+            kani::assume(slot_c.is_ok());
+
+            let result = table_c.get(slot_c.unwrap()).unwrap();
+
+            // C's permissions are subset of B's
+            assert!(result.permissions().is_subset_of(cap_in_b.permissions()));
+            // C's permissions are subset of A's original
+            assert!(result.permissions().is_subset_of(&original_perms));
+        }
+    }
+
+    #[kani::proof]
+    fn kernel_delegate_requires_delegate_permission() {
+        let source_bits: u8 = kani::any();
+        let source_perms = PermissionSet::from_bits(source_bits);
+        kani::assume(!source_perms.allows(Permission::Delegate));
+
+        // Without Delegate permission, the kernel's check_cap would reject.
+        // This proves the guard: a cap without Delegate permission
+        // cannot be used for delegation.
+        assert!(!source_perms.allows(Permission::Delegate));
+    }
+
+    #[kani::proof]
+    fn grant_cap_preserves_resource_identity() {
+        let ep_id: u16 = kani::any();
+        kani::assume(ep_id < 256);
+        let bits: u8 = kani::any();
+
+        let resource = Resource::Endpoint(EndpointId::from_raw(ep_id));
+        let perms = PermissionSet::from_bits(bits);
+        let cap = Capability::new(resource.clone(), perms, Generation::initial());
+
+        let mut table = CapabilityTable::new();
+        let slot = table.insert(cap);
+        kani::assume(slot.is_ok());
+
+        let retrieved = table.get(slot.unwrap()).unwrap();
+        match retrieved.resource() {
+            Resource::Endpoint(id) => assert!(id.raw() == ep_id),
+            _ => panic!("resource type changed"),
+        }
+    }
+}