diff --git a/crates/domain/src/memory/mod.rs b/crates/domain/src/memory/mod.rs
index adf0ddd..00f7ff1 100644
--- a/crates/domain/src/memory/mod.rs
+++ b/crates/domain/src/memory/mod.rs
@@ -58,6 +58,10 @@ impl MemoryRegion {
     pub fn generation(&self) -> &Generation {
         &self.generation
     }
+
+    pub fn revoke(&mut self) {
+        self.generation = self.generation.next();
+    }
 }
 
 pub struct RegionTable {
@@ -82,6 +86,10 @@ impl RegionTable {
         self.regions.get(id.raw() as usize).and_then(|s| s.as_ref())
     }
 
+    pub fn get_mut(&mut self, id: RegionId) -> Option<&mut MemoryRegion> {
+        self.regions.get_mut(id.raw() as usize).and_then(|s| s.as_mut())
+    }
+
     pub fn remove(&mut self, id: RegionId) -> Option<MemoryRegion> {
         self.regions.get_mut(id.raw() as usize).and_then(|s| s.take())
     }
diff --git a/crates/kernel/src/lib.rs b/crates/kernel/src/lib.rs
index a5d1b2e..9c481d3 100644
--- a/crates/kernel/src/lib.rs
+++ b/crates/kernel/src/lib.rs
@@ -160,16 +160,53 @@ impl<P: Platform> Kernel<P> {
         if !cap.permissions().allows(needed) {
             return Err(KernelError::PermissionDenied { slot, needed });
         }
+        let current_gen = self.resource_generation(cap.resource());
+        if !cap.generation().is_valid_against(&current_gen) {
+            return Err(KernelError::RevokedCapability(slot));
+        }
         Ok(cap)
     }
 
+    fn resource_generation(&self, resource: &Resource) -> Generation {
+        match resource {
+            Resource::Endpoint(id) => self
+                .endpoints
+                .get(*id)
+                .map(|ep| *ep.generation())
+                .unwrap_or_else(|| Generation::initial()),
+            Resource::Memory(id) => self
+                .regions
+                .get(*id)
+                .map(|r| *r.generation())
+                .unwrap_or_else(|| Generation::initial()),
+            _ => Generation::initial(),
+        }
+    }
+
+    pub fn revoke_resource(&mut self, resource: &Resource) {
+        match resource {
+            Resource::Endpoint(id) => {
+                if let Some(ep) = self.endpoints.get_mut(*id) {
+                    ep.revoke();
+                }
+            }
+            Resource::Memory(id) => {
+                if let Some(r) = self.regions.get_mut(*id) {
+                    r.revoke();
+                }
+            }
+            _ => {}
+        }
+    }
+
     fn grant_cap(
         &mut self,
         to: ProcessId,
         resource: Resource,
         permissions: PermissionSet,
     ) -> Result<CapSlot, KernelError> {
-        let cap = Capability::new(resource, permissions, Generation::initial());
+        let generation = self.resource_generation(&resource);
+        let cap = Capability::new(resource, permissions, generation);
         self.processes.get_mut(to)?.capabilities_mut().insert(cap)
     }
 }
diff --git a/crates/kernel/src/proofs/revocation.rs b/crates/kernel/src/proofs/revocation.rs
index 2169d11..f928f0b 100644
--- a/crates/kernel/src/proofs/revocation.rs
+++ b/crates/kernel/src/proofs/revocation.rs
@@ -1,9 +1,10 @@
 use domain::capability::{Capability, CapabilityTable};
+use domain::endpoint::Endpoint;
 use domain::resource::Resource;
 use super::{arbitrary_endpoint_cap, insert_cap};
 use types::generation::Generation;
 use types::id::EndpointId;
-use types::permission::PermissionSet;
+use types::permission::{Permission, PermissionSet};
 
 #[kani::proof]
 fn revoke_invalidates_cap_slot() {
@@ -61,3 +62,77 @@ fn grant_cap_preserves_resource_identity() {
         _ => panic!("resource type changed"),
     }
 }
+
+#[kani::proof]
+fn generation_revocation_invalidates_all_caps() {
+    let bits: u8 = kani::any();
+    let ep_id: u16 = kani::any();
+    kani::assume(ep_id < 256);
+
+    let mut endpoint = Endpoint::new(EndpointId::from_raw(ep_id));
+    let original_gen = *endpoint.generation();
+
+    let cap = Capability::new(
+        Resource::Endpoint(EndpointId::from_raw(ep_id)),
+        PermissionSet::from_bits(bits),
+        original_gen,
+    );
+
+    let mut table = CapabilityTable::new();
+    let slot = insert_cap(&mut table, cap);
+
+    assert!(table.get(slot).unwrap().generation().is_valid_against(&original_gen));
+
+    endpoint.revoke();
+    let new_gen = *endpoint.generation();
+
+    assert!(!table.get(slot).unwrap().generation().is_valid_against(&new_gen));
+}
+
+#[kani::proof]
+fn cap_created_after_revoke_is_valid() {
+    let ep_id: u16 = kani::any();
+    kani::assume(ep_id < 256);
+    let bits: u8 = kani::any();
+
+    let mut endpoint = Endpoint::new(EndpointId::from_raw(ep_id));
+    endpoint.revoke();
+    let current_gen = *endpoint.generation();
+
+    let cap = Capability::new(
+        Resource::Endpoint(EndpointId::from_raw(ep_id)),
+        PermissionSet::from_bits(bits),
+        current_gen,
+    );
+
+    assert!(cap.generation().is_valid_against(&current_gen));
+}
+
+#[kani::proof]
+fn multiple_revocations_invalidate_all_prior_caps() {
+    let ep_id: u16 = kani::any();
+    kani::assume(ep_id < 256);
+
+    let mut endpoint = Endpoint::new(EndpointId::from_raw(ep_id));
+
+    let gen0 = *endpoint.generation();
+    let cap0 = Capability::new(
+        Resource::Endpoint(EndpointId::from_raw(ep_id)),
+        PermissionSet::empty().with(Permission::Read),
+        gen0,
+    );
+
+    endpoint.revoke();
+    let gen1 = *endpoint.generation();
+    let cap1 = Capability::new(
+        Resource::Endpoint(EndpointId::from_raw(ep_id)),
+        PermissionSet::empty().with(Permission::Read),
+        gen1,
+    );
+
+    endpoint.revoke();
+    let gen2 = *endpoint.generation();
+
+    assert!(!cap0.generation().is_valid_against(&gen2));
+    assert!(!cap1.generation().is_valid_against(&gen2));
+}
diff --git a/crates/kernel/src/tests/capability.rs b/crates/kernel/src/tests/capability.rs
index 397bb8a..474d091 100644
--- a/crates/kernel/src/tests/capability.rs
+++ b/crates/kernel/src/tests/capability.rs
@@ -1,8 +1,9 @@
 use super::*;
 use crate::{SyscallOutcome, SyscallResult};
+use domain::resource::Resource;
 use domain::syscall::Syscall;
 use types::bounded::CapSlot;
-use types::permission::PermissionSet;
+use types::permission::{Permission, PermissionSet};
 use types::address::DataRef;
 
 #[test]
@@ -53,3 +54,92 @@ fn delegate_with_valid_cap_succeeds() {
         SyscallOutcome::Complete(SyscallResult::Ok)
     ));
 }
+
+// --- Generation-based revocation ---
+
+#[test]
+fn revoke_resource_invalidates_all_caps() {
+    let (mut k, pid) = kernel_with_process();
+    let ep_id = k.create_endpoint_for_test();
+
+    let cap_slot = k.grant_cap_for_test(
+        pid,
+        Resource::Endpoint(ep_id),
+        PermissionSet::empty().with(Permission::Read),
+    );
+
+    // Revoke the endpoint
+    k.revoke_resource(&Resource::Endpoint(ep_id));
+
+    // Cap is now invalid — check_cap should reject with RevokedCapability
+    let outcome = k.handle_syscall(Syscall::Receive { endpoint: cap_slot });
+    assert!(matches!(
+        outcome,
+        SyscallOutcome::Complete(SyscallResult::Error(domain::error::KernelError::RevokedCapability(_)))
+    ));
+}
+
+#[test]
+fn new_cap_after_revoke_uses_current_generation() {
+    let (mut k, pid) = kernel_with_process();
+    let ep_id = k.create_endpoint_for_test();
+
+    // Grant, revoke, grant again
+    let old_slot = k.grant_cap_for_test(
+        pid,
+        Resource::Endpoint(ep_id),
+        PermissionSet::empty().with(Permission::Read),
+    );
+
+    k.revoke_resource(&Resource::Endpoint(ep_id));
+
+    // Old cap is dead
+    let outcome = k.handle_syscall(Syscall::Receive { endpoint: old_slot });
+    assert!(matches!(
+        outcome,
+        SyscallOutcome::Complete(SyscallResult::Error(domain::error::KernelError::RevokedCapability(_)))
+    ));
+
+    // New cap with current generation works
+    let new_slot = k.grant_cap_for_test(
+        pid,
+        Resource::Endpoint(ep_id),
+        PermissionSet::empty().with(Permission::Read),
+    );
+
+    let outcome = k.handle_syscall(Syscall::Receive { endpoint: new_slot });
+    // Should block (no sender), not error — proving the cap is valid
+    assert!(matches!(outcome, SyscallOutcome::BlockCaller(_)));
+}
+
+#[test]
+fn revoke_does_not_affect_other_resources() {
+    let (mut k, pid) = kernel_with_process();
+    let ep1 = k.create_endpoint_for_test();
+    let ep2 = k.create_endpoint_for_test();
+
+    let slot1 = k.grant_cap_for_test(
+        pid,
+        Resource::Endpoint(ep1),
+        PermissionSet::empty().with(Permission::Read),
+    );
+    let slot2 = k.grant_cap_for_test(
+        pid,
+        Resource::Endpoint(ep2),
+        PermissionSet::empty().with(Permission::Read),
+    );
+
+    // Revoke only ep1
+    k.revoke_resource(&Resource::Endpoint(ep1));
+
+    // ep1 cap is revoked
+    let outcome = k.handle_syscall(Syscall::Receive { endpoint: slot1 });
+    assert!(matches!(
+        outcome,
+        SyscallOutcome::Complete(SyscallResult::Error(domain::error::KernelError::RevokedCapability(_)))
+    ));
+
+    // ep2 cap still works
+    let outcome = k.handle_syscall(Syscall::Receive { endpoint: slot2 });
+    assert!(matches!(outcome, SyscallOutcome::BlockCaller(_)));
+}
diff --git a/crates/types/src/generation.rs b/crates/types/src/generation.rs
index 34b0c4d..991208a 100644
--- a/crates/types/src/generation.rs
+++ b/crates/types/src/generation.rs
@@ -13,4 +13,9 @@ impl Generation {
     pub fn is_valid_against(&self, current: &Generation) -> bool {
         self == current
     }
+
+    #[cfg(kani)]
+    pub fn from_raw(value: u32) -> Self {
+        Self(value)
+    }
 }
diff --git a/crates/types/src/lib.rs b/crates/types/src/lib.rs
index f356f1d..cbfc06b 100644
--- a/crates/types/src/lib.rs
+++ b/crates/types/src/lib.rs
@@ -6,4 +6,6 @@ pub mod generation;
 pub mod id;
 pub mod macros;
 pub mod permission;
+#[cfg(kani)]
+pub mod proofs;
 pub mod time;
diff --git a/crates/types/src/permission.rs b/crates/types/src/permission.rs
index 21a23a3..9df42f0 100644
--- a/crates/types/src/permission.rs
+++ b/crates/types/src/permission.rs
@@ -40,4 +40,9 @@ impl PermissionSet {
     pub fn is_subset_of(&self, other: &PermissionSet) -> bool {
         self.0 & other.0 == self.0
     }
+
+    #[cfg(kani)]
+    pub fn from_bits(bits: u8) -> Self {
+        PermissionSet(bits)
+    }
 }