Explore formal verification of storage encoding with Kani #627

Summary

Explore adding formal verification to Minigraf, in a narrow form. The goal is not to prove the whole engine. The goal is to prove a few small, pure, high-risk pieces of the storage layer for every input, and run those proofs in scheduled CI.

Background

A deductive verifier checks code against a written spec (preconditions, postconditions, loop invariants) by turning it into logic formulas and handing them to an SMT solver. It does not run the code. If the proof goes through, the property holds for every input. If not, the solver returns a counterexample.

The Rust options today:

• Verus: closest to a full deductive verifier (spec, proof and exec modes, ghost code, Z3). Code must live inside a verus! macro, so it is not plain Rust.
• Creusot: deductive, contracts as attributes on plain Rust, Why3 backend.
• Prusti: contracts on plain Rust, Viper backend, checks for panics by default.
• Kani: bounded model checker, not deductive. Runs on unchanged Rust. Proves a property for every input up to a bound.
• Aeneas: translates Rust to Lean for kernel-checked proofs.

Why not a full deductive verifier

• Verus would mean rewriting core modules into its dialect and keeping two mental models of the code.
• Creusot or Prusti on the B+tree, WAL and Datalog engine would need many invariants and helper lemmas. That is a large, ongoing maintenance cost for a solo-maintained project.
• The current test posture already covers much of the risk: the WAL is fuzzed and fault-injected, decoding is fuzzed against panics, the query engine is differentially tested, bi-temporal semantics are property-tested, and the soak suite runs on a schedule.

Where a verifier pays off

Fuzzing is good at finding crashes. It is weaker at proving that byte-level code is exactly right, for example that an encoding never loses information or never breaks sort order. Those bugs are silent. A proof harness that states the exact property closes that gap.

Candidate targets:

1. encode_value in src/storage/index.rs
   • Order-preserving: for all a, b, a.cmp(&b) == encode_value(&a).cmp(&encode_value(&b)) (with NaN handled per the canonical encoding).
   • Injective: different values never encode to the same bytes (apart from canonical NaN).
   • The sign-bit flip for Integer and the bit tricks for Float are exactly the kind of code where a proof is cheap and a bug is silent.
2. Index key ordering: the derived Ord on EavtKey, AevtKey, AvetKey and VaetKey agrees with the intended sort order, and keys built from two different facts never collide.
3. Packed pages (src/storage/packed_pages.rs): read_slot after pack_facts returns the original fact, and all offset and slice arithmetic stays in bounds with no overflow.
4. WAL framing (src/wal.rs): decoding a serialized entry returns the original tx_count and facts, and decoding any byte string never reads out of bounds.

Recommendation

Use Kani for these targets.

• Runs on unchanged Rust. Harnesses live behind #[cfg(kani)], so the public API and normal build do not change.
• A harness reads like a property test, but covers every input within the bound:

#[cfg(kani)]
#[kani::proof]
#[kani::unwind(10)]
fn encode_value_preserves_order() {
    let a: Value = kani::any();
    let b: Value = kani::any();
    // bound string/keyword lengths here with kani::assume
    assert_eq!(a.cmp(&b), encode_value(&a).cmp(&encode_value(&b)));
}

• The limit is that it is bounded. "All strings up to 8 bytes" is not "all strings". For encoding code that treats every byte the same way, a small bound usually catches the real bugs.

Revisit Verus or Creusot only if Kani harnesses prove cheap to keep and there is a specific module where a full functional proof would be worth the cost.

CI

• Kani is slow (often minutes per harness). Keep it out of the per-PR path at first.
• Add a scheduled workflow (daily, or alongside the existing scheduled jobs such as soak.yml) using the official Kani GitHub Action.
• If one or two harnesses stay fast, move them into PR checks later.
• Kani pins its own nightly toolchain and can lag new Rust features or some dependencies. Expect some upkeep.

Suggested plan

• Add one Kani harness for encode_value (order and injectivity). Measure run time and effort.
• Add a scheduled CI workflow that runs all harnesses.
• If the first harness is cheap and useful, add harnesses for packed pages and WAL framing.
• Write down findings and decide whether a deductive tool (Verus or Creusot) is worth a follow-up issue.

Out of scope

• Proofs of the Datalog engine, magic sets or bi-temporal query semantics. Differential and property tests stay the main defense there.
• Rewriting any module into a verifier-specific dialect.

Generated by Claude Code