2026-11-05 –, Lotus Stage 2
Specs for confidential systems make security claims in prose: value is conserved, no note can be spent twice. This talk is an experience report from machine-checking those claims for an open source shielded pool spec in Lean 4: what verification actually involves, what it costs a small team today, and what's still open.
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?
I'm an engineer and amateur cook, passionate about privacy, cryptography, and distributed systems. I write about the intersection of technology and society, with a focus on building systems that preserve human autonomy and privacy.
Currently, I work with EthSystems to onboard institutions to Ethereum in a way that's performant and confidential, and being pragmatic about the tradeoffs that come with private systems.