Formally Verifying a Shielded Pool in Lean 4

The worst shielded pool bugs are soundness bugs: quietly creating value out of nothing. Zcash's counterfeiting bug survived multiple audits for years; with Ironwood, Zcash turned to machine-checked Lean proofs that counterfeiting is impossible at the spec level. Ethereum's shielded pools have nothing comparable yet.

We're running an experiment to close that gap: model our open source shielded pool spec in Lean 4 and prove value conservation and no double-spend, scoped to integrity rather than privacy. More broadly, every confidential system institutions rely on makes claims like these; spec-level proofs are a reusable way to back them.

The talk is educational as much as a report: how a prose spec becomes a Lean model, what a conservation proof looks like, where modeling goes wrong, and what it cost. No formal methods background needed. You should leave with a working model of spec-level verification, and a question: when should specs stop asserting properties and start proving them?

Speakers: Aaryamann Challani

Track: Security