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 the VM, fork, snapshot, and device modules).
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 budget 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. Aeneas (via Charon) translates it to Lean, where theorems about the model — budget invariants, eviction ordering, protection being honored — are proved and re-checked whenever the model changes:
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, 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 (≤25k lines for VMM + shim). See the repo’s verification setup for the Lean sources and axiom allowlist.