diff --git a/crates/kernel/src/proofs.rs b/crates/kernel/src/proofs.rs
index 476eb4d..23ec2f7 100644
--- a/crates/kernel/src/proofs.rs
+++ b/crates/kernel/src/proofs.rs
@@ -1,6 +1,7 @@
 #[cfg(kani)]
 mod kani_proofs {
     use domain::capability::{Capability, CapabilityTable};
+    use domain::message::{Message, MAX_MESSAGE_WORDS};
     use domain::resource::Resource;
     use types::bounded::CapSlot;
     use types::generation::Generation;
@@ -180,4 +181,160 @@ mod kani_proofs {
             _ => panic!("resource type changed"),
         }
     }
+
+    // --- Complete mediation: every resource-accessing syscall checks caps ---
+
+    #[kani::proof]
+    fn handle_send_rejects_without_execute_permission() {
+        let bits: u8 = kani::any();
+        let ep_id: u16 = kani::any();
+        kani::assume(ep_id < 256);
+
+        let perms = PermissionSet::from_bits(bits);
+        kani::assume(!perms.allows(Permission::Execute));
+
+        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().allows(Permission::Execute));
+    }
+
+    #[kani::proof]
+    fn handle_receive_rejects_without_read_permission() {
+        let bits: u8 = kani::any();
+        let ep_id: u16 = kani::any();
+        kani::assume(ep_id < 256);
+
+        let perms = PermissionSet::from_bits(bits);
+        kani::assume(!perms.allows(Permission::Read));
+
+        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().allows(Permission::Read));
+    }
+
+    #[kani::proof]
+    fn missing_cap_always_rejected() {
+        let slot_val: u8 = kani::any();
+        kani::assume(slot_val <= 63);
+        let slot = CapSlot::new(slot_val).unwrap();
+
+        let table = CapabilityTable::new();
+        assert!(table.get(slot).is_err());
+    }
+
+    // --- Message delivery integrity ---
+
+    #[kani::proof]
+    fn message_survives_pending_storage_roundtrip() {
+        let w0: usize = kani::any();
+        let w1: usize = kani::any();
+        let w2: usize = kani::any();
+        let w3: usize = kani::any();
+
+        let original = Message::from_words([w0, w1, w2, w3]);
+
+        let mut pending: [Option<Message>; 4] = [const { None }; 4];
+        let idx: usize = kani::any();
+        kani::assume(idx < 4);
+
+        pending[idx] = Some(original);
+
+        let retrieved = pending[idx].take();
+        assert!(retrieved.is_some());
+
+        let msg = retrieved.unwrap();
+        assert!(msg.word(0) == w0);
+        assert!(msg.word(1) == w1);
+        assert!(msg.word(2) == w2);
+        assert!(msg.word(3) == w3);
+    }
+
+    #[kani::proof]
+    fn message_storage_does_not_cross_slots() {
+        let w_a: usize = kani::any();
+        let w_b: usize = kani::any();
+        kani::assume(w_a != w_b);
+
+        let msg_a = Message::from_words([w_a, 0, 0, 0]);
+        let msg_b = Message::from_words([w_b, 0, 0, 0]);
+
+        let mut pending: [Option<Message>; 4] = [const { None }; 4];
+        pending[0] = Some(msg_a);
+        pending[1] = Some(msg_b);
+
+        let retrieved_a = pending[0].take().unwrap();
+        let retrieved_b = pending[1].take().unwrap();
+
+        assert!(retrieved_a.word(0) == w_a);
+        assert!(retrieved_b.word(0) == w_b);
+    }
+
+    // --- Revocation completeness ---
+
+    #[kani::proof]
+    fn revoke_invalidates_cap_slot() {
+        let bits: u8 = kani::any();
+        let ep_id: u16 = kani::any();
+        kani::assume(ep_id < 256);
+
+        let perms = PermissionSet::from_bits(bits);
+        let cap = Capability::new(
+            Resource::Endpoint(EndpointId::from_raw(ep_id)),
+            perms,
+            Generation::initial(),
+        );
+
+        let mut table = CapabilityTable::new();
+        let slot = table.insert(cap);
+        kani::assume(slot.is_ok());
+        let slot = slot.unwrap();
+
+        assert!(table.get(slot).is_ok());
+        table.remove(slot).unwrap();
+        assert!(table.get(slot).is_err());
+    }
+
+    #[kani::proof]
+    fn revoke_does_not_affect_other_slots() {
+        let bits_a: u8 = kani::any();
+        let bits_b: u8 = kani::any();
+
+        let cap_a = Capability::new(
+            Resource::ProcessCreate,
+            PermissionSet::from_bits(bits_a),
+            Generation::initial(),
+        );
+        let cap_b = Capability::new(
+            Resource::Endpoint(EndpointId::from_raw(0)),
+            PermissionSet::from_bits(bits_b),
+            Generation::initial(),
+        );
+
+        let mut table = CapabilityTable::new();
+        let slot_a = table.insert(cap_a);
+        let slot_b = table.insert(cap_b);
+        kani::assume(slot_a.is_ok() && slot_b.is_ok());
+        let slot_a = slot_a.unwrap();
+        let slot_b = slot_b.unwrap();
+
+        table.remove(slot_a).unwrap();
+
+        assert!(table.get(slot_a).is_err());
+        assert!(table.get(slot_b).is_ok());
+        assert!(*table.get(slot_b).unwrap().permissions() == PermissionSet::from_bits(bits_b));
+    }
 }