Module verification 

Formal Verification Module

Provides model-checking infrastructure and proof harnesses for verifying critical kernel invariants: boot chain integrity, IPC correctness, memory allocator safety, and capability system soundness.

Modules

alloc_proofs

Verified Memory Allocator

boot_chain

Verified Boot Chain

cap_proofs

Capability Formal Model

ipc_proofs

Formally Verified IPC