diff --git a/crates/domain/src/proofs.rs b/crates/domain/src/proofs.rs
index dec8cc3..864669f 100644
--- a/crates/domain/src/proofs.rs
+++ b/crates/domain/src/proofs.rs
@@ -3,7 +3,7 @@ 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::bounded::Priority;
     use types::generation::Generation;
     use types::id::{CoreId, EndpointId, ProcessId, ThreadId};
     use types::permission::{Permission, PermissionSet};
@@ -137,7 +137,7 @@ mod kani_proofs {
         kani::assume(prio_val <= 31);
         let prio = Priority::new(prio_val).unwrap();
 
-        let thread = Thread::new(
+        let mut thread = Thread::new(
             ThreadId::from_raw(0),
             ProcessId::from_raw(0),
             prio,
diff --git a/crates/types/src/proofs.rs b/crates/types/src/proofs.rs
new file mode 100644
index 0000000..4d43345
--- /dev/null
+++ b/crates/types/src/proofs.rs
@@ -0,0 +1,83 @@
+#[cfg(kani)]
+mod kani_proofs {
+    use crate::bounded::{CapSlot, PageCount, Priority};
+    use crate::generation::Generation;
+    use crate::permission::PermissionSet;
+
+    #[kani::proof]
+    fn restrict_to_never_escalates() {
+        let a: u8 = kani::any();
+        let b: u8 = kani::any();
+
+        let original = PermissionSet::from_bits(a);
+        let restrictor = PermissionSet::from_bits(b);
+        let result = original.restrict_to(&restrictor);
+
+        assert!(result.is_subset_of(&original));
+        assert!(result.is_subset_of(&restrictor));
+    }
+
+    #[kani::proof]
+    fn restrict_to_is_commutative_in_result() {
+        let a: u8 = kani::any();
+        let b: u8 = kani::any();
+
+        let set_a = PermissionSet::from_bits(a);
+        let set_b = PermissionSet::from_bits(b);
+
+        let ab = set_a.restrict_to(&set_b);
+        let ba = set_b.restrict_to(&set_a);
+
+        assert!(ab == ba);
+    }
+
+    #[kani::proof]
+    fn empty_permission_set_restricts_everything_to_empty() {
+        let a: u8 = kani::any();
+        let set = PermissionSet::from_bits(a);
+        let empty = PermissionSet::empty();
+
+        let result = set.restrict_to(&empty);
+        assert!(result == empty);
+    }
+
+    #[kani::proof]
+    fn generation_next_always_invalidates() {
+        let value: u32 = kani::any();
+        let current = Generation::from_raw(value);
+        let next = current.next();
+
+        assert!(!current.is_valid_against(&next));
+    }
+
+    #[kani::proof]
+    fn capslot_always_valid_index() {
+        let value: u8 = kani::any();
+        if let Some(slot) = CapSlot::new(value) {
+            assert!(slot.value() <= 63);
+        }
+    }
+
+    #[kani::proof]
+    fn capslot_rejects_out_of_range() {
+        let value: u8 = kani::any();
+        kani::assume(value > 63);
+        assert!(CapSlot::new(value).is_none());
+    }
+
+    #[kani::proof]
+    fn priority_always_fits_in_bitmap() {
+        let value: u8 = kani::any();
+        if let Some(prio) = Priority::new(value) {
+            assert!((prio.value() as u32) < 32);
+        }
+    }
+
+    #[kani::proof]
+    fn page_count_is_always_nonzero() {
+        let value: u16 = kani::any();
+        if let Some(count) = PageCount::new(value) {
+            assert!(count.value() >= 1);
+        }
+    }
+}