Lean 4 Proofs
Machine-checked correctness proofs for the algorithms Nucleus is built on. 26 files, 70 theorems, zero uses of sorry. Each proof covers a Lean model of the algorithm — MVCC, B-tree, WAL, Raft and more — correct for every input, not just the cases a test happened to try.
Don't just test. Prove.
The algorithms that can't get this wrong.
Nucleus handles your transactions, replicates your data, and signs your tokens — tests alone aren't enough for that kind of code. Neutron's Lean 4 suite contains machine-checked proofs of the core algorithms: MVCC snapshot isolation, B-tree invariants, write-ahead log durability, Raft safety, HMAC verification, Bloom filter false-positive bounds, LRU eviction correctness, and sliding-window rate limiting. Every proof compiles with zero use of sorry — against precise Lean models of each algorithm, with a handful of foundational facts (like SHA-256 collision resistance) declared as explicit, auditable axioms.
namespace Nucleus.MVCC
/-- Two transactions that read the same key must see the same value
under snapshot isolation, regardless of concurrent writes. -/
theorem snapshot_read_consistency
(t₁ t₂ : Txn) (k : Key) (db : Database)
(h_same_snapshot : t₁.snapshot = t₂.snapshot) :
t₁.read db k = t₂.read db k := by
unfold Txn.read
rw [h_same_snapshot]
rfl
end Nucleus.MVCCsorry anywhere in the suite. The facts we don't derive from scratch — bitwise identities, standard crypto assumptions — are declared as explicit axioms you can read and audit, not hidden.| Unit tests | Property tests | Lean 4 proof | |
|---|---|---|---|
| Input coverage | Hand-picked cases | Random cases | All possible inputs |
| Correctness | Likely correct | Probably correct | Mathematically correct |
| Stays correct | Until refactor | Until refactor | Forever (proof is permanent) |
| Finds edge cases | If you thought of them | Eventually | Cannot exist by construction |
| Runtime cost | Zero | Zero | Zero |
Where this shows up in Neutron
Every algorithm modeled here is one Nucleus runs. The B-tree is the SQL index. The WAL is every durable write. Raft runs replication. HMAC signs every JWT. The proofs don't certify the compiled binary — they pin down the designs it's built on, so the parts that are hardest to get right are specified and machine-checked instead of improvised.
What about my application code?
You don't need to write Lean to use Nucleus — the proofs are ours to maintain. For your own code, Neutron's verification overview covers Kani (bounded model checking for Rust), Shuttle (concurrency testing), Verus (SMT verification), and Quint (protocol modeling). Different tools for different problems.
Part of a bigger system
Lean sits underneath Nucleus. Your app talks to Nucleus. Nucleus runs the algorithms whose designs are proven in Lean. The proof doesn't replace the tests on the Rust — it means the algorithm those tests exercise is known, mathematically, to be sound.