Skip to main content
k7d uses formal methods where they pay off — selected critical pieces are machine-checked, not the whole runtime. This is deliberately not a claim that “k7d is proven correct”; it is a claim that the two most consequence-laden pieces of logic have proofs attached, and that those proofs run in CI.

​
Kani: the unsafe and arithmetic paths

A VMM is a machine for doing address arithmetic next to unsafe blocks: guest-physical to host-virtual translation, initrd placement, GDT encoding, page-table entries, dirty-bitmap indexing. A single off-by-one silently corrupts a guest. Kani is a bounded model checker for Rust: it explores every input within a bound and proves no panic, overflow, or out-of-bounds access occurs. Proof harnesses are co-located with the code they verify — #[cfg(kani)] modules with #[kani::proof] functions at the bottom of vm.rs, fork.rs, snapshot.rs, block.rs (virtio-blk request-header parsing and I/O byte-offset bounds), and mptable.rs (the SMP MP table fits below 640 KiB and its size is monotone in the vCPU count).
Complementing Kani, every unsafe block carries a // SAFETY: comment (lint-enforced), Miri runs over the non-KVM unit tests, and libFuzzer runs over the agent protocol and virtio-blk request parsing.

​
Aeneas → Lean: the tree model

The snapshot tree’s budget and eviction bookkeeping decides which VMs live, which get suspended, and which state gets deleted. A bookkeeping bug here means OOM-ing the host or evicting a protected winner mid-training-run. That logic is factored into a pure, side-effect-free Rust module (tree_model.rs). Aeneas (via Charon) translates it to Lean, where theorems are proved and re-checked whenever the model changes:
The proofs are grouped by what a failure would cost: The theorems are stated against hand-written Lean mirrors; a separate equivalence layer (verif/Verif/Equiv/) proves the mirrors match the Aeneas-generated translation of the Rust, so a regeneration that renames a generated identifier breaks only that layer, never the theorems. The translation is guarded: any Rust primitive that Aeneas cannot model lands in the generated Lean as a bodyless axiom, and the build fails if an axiom appears that is not on an explicit allowlist. New unprovable constructs must be refactored away rather than silently assumed.

​
What is not verified

Everything else: the virtio device implementations, the KVM run loop, the network dataplane and jail, the clock-warp machinery, the shim, the agent. Those rely on the conventional arsenal — the type system, integration tests with enforced latency budgets, fuzzing, Miri, and a deliberately small codebase (≤30k lines for VMM + shim). See the repo’s verification setup for the Lean sources and axiom allowlist.