Formally Verifying a Shielded Pool in Lean 4

Duration: NaN:NaN:NaN

Speaker: Oskar Thoren, Aaryamann Challani

Type: Talk

Expertise: Some familiarity with the topic

Event: Devcon

Date: Nov 2026

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?