The Supervisionary proof-checking kernel, or: a work-in-progress toward proof-g
summary
A prototype proof-checking kernel implemented as a Rust implementation running as a WebAssembly host exposes a 75-call syscall interface (about 75 syscalls) that manages private kernel heaps of objects (types, terms, theorems) via opaque handles; the repo contains most of the kernel and libsupervisionary for automation clients, and core operations (allocate, register combinations, reflexivity) work end-to-end. Novel claim: theorem handles act as dynamic capability policies that the kernel checks to gate file, RNG or syscall effects.
AI-written summary · about
chapters (4)
related talks
23mApplying Formal Verification to Microkernel IPC at Meta
50mTrust but Verify: Scaling Deductive Verification with Abstract Interpretation
01h 05mKeynote: Can we reason about the security of concurrent systems code?
28mLightweight Hypervisor Verification: Putting the Hardware Burger on a Diet
21mEnhancing Symbolic Execution with Machine-Checked Safety Proofs
46mA Maintainable, Scalable, and Verifiable SW Qualification Approach for Automotive in Linux
19mRex: Closing the language-verifier gap with safe and usable kernel extensions
38mHow I started chasing speculative type confusion bugs in the kernel and ended up wi...