tool

Lean 4 Proofs

Machine-checked correctness proofs for the algorithms Nucleus depends on. 26 proof files, zero uses of sorry, 100% proven. When the compiler accepts the file, the algorithm is right — for all inputs, forever.

Don't test. Prove.

Available

26Proof Files

0Uses of sorry

100%Proven

Lean 4Prover

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.

proofs/MVCC.lean
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.MVCC
A sample of what's in the suite. The full file proves snapshot isolation.

MVCC & B-tree

Snapshot isolation rules proven. B-tree structural invariants (ordering, balance, split correctness) proven.

WAL & Raft

Write-ahead log durability across crashes proven. Raft leader election and log safety proven from the original TLA+ spec.

Crypto primitives

HMAC message authentication proven correct against the RFC 2104 spec. Constant-time comparison proven timing-safe.

Data structures

Bloom filter false-positive bound proven. LRU eviction ordering proven. Sliding-window rate limiter proven fair.

Zero sorry

Every theorem in the suite has a complete proof. sorry (the "trust me" keyword) appears nowhere. When the file compiles, the theorem is proven.

Compiled to native

Lean 4 is a programming language, not just a proof assistant. The same definitions that we prove correct compile to C and run in production.

	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 proven here is live in Nucleus. The B-tree is the SQL index. The WAL is every durable write. Raft runs replication. HMAC signs every JWT. When your app writes to Nucleus, it's running algorithms that have machine-checked proofs of correctness sitting next to the source.

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 algorithms whose correctness is proven in Lean. Three layers, one property: when a query returns a row, it's the right row.