Some invariants are simple enough to state in one line and simple enough to get wrong in a hundred ways: the books balance, the transcript cannot be forged, the quorum arithmetic adds up. Tests probe such invariants on examples. A proof checks them universally. The interesting engineering question is where a proof fits in a shipping product without becoming a research project that blocks releases.
the claim
A proof assistant such as Lean takes the statement "for every ledger of this shape, debits equal credits" and produces a derivation a mechanical checker accepts or rejects. Once the checker accepts, the claim is true for every input the theorem covers: not on the examples a test happened to pick, but on all of them.
That is a different kind of evidence than a test. A test is a sample; a proof is a census. The two are complementary, and treating either as a replacement for the other is how teams end up proving the wrong theorem or testing the same case a thousand times.
what a lean proof buys
The portfolio's pattern is narrow and deliberate: proofs over the laws that are expensive to get wrong and cheap to formalize.
Gobstopper keeps transcript invariants in Lean. Its vault holds copies of agent sessions; the claim that compaction preserved a transcript's structure is a property of the transformation, not of any particular session, so it belongs in a theorem. The Lean side states the structural law; the Rust side implements the transform; a correspondence check keeps the two honest.
vhalla's quorum reasoning is the same shape. A delivery that claims member acceptance has to satisfy arithmetic over how many members acknowledged what. Off-by-one in quorum counting is the classic distributed-systems hole, and it is exactly the kind of arithmetic a proof checker is good at: small statement, universal quantification, no environment.
The spike for algal-cloud's money laws follows the same logic: if a ledger of holds and captures is ever to hold real value, "debits equal credits" should be a theorem, not a wish. That work is a spike, not a launched product; the claim here is about the technique, not the product.
how it runs in ci
The working pattern treats the proof checker as a build step with a budget. The proofs live beside the code they constrain; CI runs the checker the way it runs tests; a failed proof blocks the same way a failed test does. The important operational property is that the checker is deterministic: the same proof either always checks or always fails, so there is no flaky-proof category to triage.
The equally important property is the correspondence boundary. A Lean proof about "the transcript transform preserves structure" says nothing unless the Rust code actually implements that transform. The projects keep an explicit correspondence layer: the Lean statement names the law, the implementation names the function that claims it, and the test suite pins the two together so one cannot drift from the other silently.