Proving the fork: Kani, Aeneas, and budgets as CI

Formal methods where they pay off — and a precise account of where I deliberately stopped.

August 2026 · ~11 min read

Let me set the scope honestly before the first proof appears, because "formally verified VMM" is a claim I am specifically not making. k7d machine-checks selected critical pieces — the unsafe memory arithmetic that a fork depends on, and the snapshot tree's budget/eviction model — not the whole runtime. The rest of the correctness story is ordinary engineering: integration tests, fuzzing, and latency budgets enforced in CI. This post is about how those layers fit together, and why the two places that got real proofs are the two places where testing structurally can't reach.

Why these two places

The common thread of this series' bugs (the repo's CHALLENGES.md has the full catalog) is that fork bugs fail silently. A wrong dirty-page union doesn't crash — it resurrects stale bytes in some future fork. An eviction off-by-one doesn't crash — it deletes the protected winner of a six-hour search, once, under memory pressure. Tests catch what you thought to assert on inputs you thought to try. For code whose failure mode is "quietly wrong, rarely, later", I wanted a stronger word than "tested".

Two candidates cleared the cost-benefit bar:

The unsafe memory math. Address arithmetic, page-range calculations, the chunking that parallel memory copies are driven by. Small, pure, and any error is guest-memory corruption.
The tree bookkeeping. Budget accounting, LRU victim selection, protection exemption — the logic that decides which VM the daemon is allowed to kill on its own (Part 5). Small, pure, and any error deletes the wrong VM.

Both share the property that makes verification tractable: they're deterministic logic with no I/O, extracted into functions a tool can reason about exhaustively. That's not luck — the code was shaped to make it true, and reshaping code to be provable turns out to improve it anyway.

Layer one: Kani on the unsafe paths

Kani does bounded model checking for Rust: a proof harness declares symbolic inputs ("any u64", "any size in 1..=8"), and Kani + CBMC exhaustively verify that no input within bounds can cause a panic, an overflow, or a memory-safety violation. Not "10,000 random inputs" — all inputs, within the harness's bounds. The harnesses live next to the code they check and run via make kani; they cover selected unsafe and address-arithmetic paths in the memory/fork machinery.

Kani also taught me its own lesson about code shape, the hard way. A harness for the parallel-copy chunking originally verified a helper that returned a Vec of chunk ranges with a symbolic capacity — and CBMC promptly ran out of memory, because a heap allocation whose size is symbolic forces the model checker to consider the allocator's behavior for every candidate capacity. The fix was to refactor the helper into a pure copy_chunk_size(mem_size, max_chunks) → u64 and drive the copy loop off plain arithmetic — no Vec at runtime either. The proof went from OOM to verifying in seconds, and the production code got simpler. This kept happening: the version of the code that can be verified is usually the version you should have written anyway.

Layer two: Aeneas → Lean on the tree model

Kani answers "does this arithmetic ever panic". For the eviction model I wanted a functional-correctness statement: the algorithm never selects a protected node as a victim, and the budget math is right. That needs a proof assistant.

The pipeline: the tree bookkeeping lives in one Rust file (tree_model.rs), deliberately free of I/O and clever borrows. Charon extracts it to an intermediate representation; Aeneas translates that into pure Lean functions; and the theorems in verif/ are proved against hand-written Lean mirrors of the same logic, with equivalence lemmas tying the generated code to the mirrors. make verif-gen verif-build regenerates and re-proves the lot; CI runs it whenever tree_model.rs changes, so the proof can't drift from the code it's about.

fig 1: the verification stack. proofs for the two silent-failure hotspots, an axiom guard so the proofs can't weaken unnoticed, and budget assertions so the performance claims can't rot.

Getting Rust through Aeneas imposed a discipline that's interesting in its own right. Aeneas's borrow-tracking symbolic execution must join the environments of every if/match arm, and a shared borrow held across arms — or a &&-chain where each conjunct re-borrows — produces joins it can't reconcile, even when rustc is perfectly happy. So tree_model.rs follows house rules: copy scalar fields to locals before branching, evaluate eligibility conjuncts into named bools, no reference lives across an arm boundary. Purely mechanical, no semantic change — and, once again, the constrained version is more readable than the original. The proofs themselves cost real effort in tactic work (the repo's CHALLENGES.md records the hours), but the model is small enough that the total stayed sane.

The axiom allowlist

Here's the failure mode nobody warns you about, and the reason I'd call this section the most transferable part of the post. When Aeneas meets a Rust primitive its Lean standard library doesn't model, it doesn't fail — it emits an axiom. An axiom is an assumption: "trust me, this exists". Anything your generated code touches through an axiom is a hole in the proof, and the build stays green.

I hit this concretely: u64::saturating_mul had no Lean model, and the derived Clone for a struct containing Option<u64> went through an Option::clone the extraction left abstract. Both arrived as axioms; both made "this function never panics" formally unprovable in a way no error message announces. The fixes were semantics-preserving Rust rewrites — an explicit overflow guard instead of saturating_mul, a manual field-wise Clone — verified by the equivalence theorems themselves.

fig 2: the axiom guard. an unmodelled primitive doesn't fail the extraction — it quietly becomes an assumption, which is why the allowlist diff is a build gate rather than a code review habit.

But the standing rule matters more than the instances: grep the generated Lean for axiom, and treat every hit as a bug until proven otherwise. That rule is now automated — a CI script diffs the axioms in the generated file against a committed allowlist and fails the build on any new one. Adding to the allowlist requires a human to write down, in a reviewed file, "we are choosing to assume this". Without a guard like this, a proof can weaken over time without anyone noticing.

Layer three: the unglamorous rest

Below the proofs, the ordinary machinery, each piece scoped to what it's actually good at:

Fuzzing on the protocol surfaces — the guest agent's message parsing and the daemon's API — where the input space is adversarial bytes rather than logic. Runs as a make target (make remote-fuzz) with a time budget, not a research project.
Miri on the non-KVM unit tests, catching undefined behavior in the pure-Rust paths that Kani's harnesses don't cover.
Integration tests as the spec. Every behavioral claim in this series — TLS survives the fork, the source keeps answering, forks can't see each other — is an assertion in a test that runs against real KVM on the real node, k3s and all.

Latency budgets are CI, too

One more thing gets the assertion treatment, and I consider it part of verification in the same spirit: the performance claims. Every number this series has quoted lives in one Rust file of budget constants; every budget is enforced by an integration test (fork < 50 ms, cluster fork < 1 s, 50-fork batch < 20 s, and so on down to agent ping RTT). If a refactor regresses the fork path past its budget, CI goes red before the README goes wrong. Benchmark tables rot; assertions don't. Budgets sit at roughly 2× typical, and where one is deliberately generous — the full suite runs serially with shared KVM state, which inflates tails — LATENCY_BUDGETS.md says so in as many words rather than quietly widening the gap.

What this does and doesn't buy

fig 3: the honest scope. two small components are machine-checked because their failures are silent, rare and catastrophic; the rest of the codebase gets ordinary engineering.

Scope, stated plainly, both directions. The proofs do not cover: the KVM ioctl sequences, the virtio device implementations, the network plumbing, the containerd shim — the majority of the ≤25k lines, guarded by tests and fuzzing, not theorems. A security audit hasn't happened yet; a proof of the eviction model is not a proof the daemon has no bugs.

What they do buy: the two components whose failures are silent, rare, and catastrophic are exhaustively checked — for all inputs within bounds, not all inputs I thought of. The eviction logic that kills VMs autonomously under budget pressure provably cannot select a protected node. The address arithmetic under every fork provably cannot overflow or panic. And the proof infrastructure is wired so that the proofs can't silently detach from the code (regeneration in CI) or hollow out from within (the axiom guard).

For a young project making strong claims, that's the deal I'd want as a reader: strong words only where the machine checked them, plain words everywhere else.

End of series

That's the whole arc: why RL needs identical environments (Part 1), why the existing tools don't fork a running cluster (Part 2), the 45-second disk-only attempt that taught me the real problem (Part 3), the VMM (Part 4), the budgeted tree (Part 5), and the verification (this one).

What's next, per the roadmap: a proper config file for the daemon, re-enabling the stock k3s add-ons (CoreDNS, ingress) in the benchmark fixture, and cross-node fork. The code is Apache-2.0 at github.com/katakate/k7d, small enough to actually read, with docs at docs.katakate.org. Would love feedback, and contributors — the roadmap is clear and open. If you train agents on infrastructure, try it and tell me what breaks.