Whitepaper Reading Club: Formal Verification in Cryptography
Formal Verification in Cryptography
You’ve probably heard plenty about formal verification, autoformalization, and Lean in the context of AI and mathematics. But what might it take for machine-checked proofs to become a routine part of secure cryptographic research? And how much of the work from a paper’s security argument on invariants can we now automate and autoformalize into a verified implementation?
Join us for a discussion of what formal verification makes possible today. We’ll explore how researchers formalize security arguments, make assumptions explicit, and check that implementations satisfy their specifications. We’ll also discuss where AI is making this work more accessible, what still requires specialist judgment, and what these tools guarantee in practice on circuits, code, and proofs.
Papers:
Format
Short introduction and context setting to start.
A short walkthrough of the paper and its key ideas.
Questions and discussion grounded in the original source.
Moderator-led discussion with no promotions.
Session Guides:
Kobi Gurkan is an applied cryptographer at zkSecurity, focusing on zero-knowledge proofs and threshold cryptography. He previously served as Partner and Head of Research at Bain Capital Crypto and founded Geometry Research. His earlier work includes leading cryptography at Celo and conducting research at the Ethereum Foundation.
Abhi Shah works on scalable formal verification and holds a PhD in Computer Science from Columbia. His past program analysis experience includes Google X, Amazon, Bloomberg and MIT Lincoln Laboratory.
About Whitepaper Reading Club
We are a community of founders, researchers, and builders across Singapore, Malaysia, San Francisco, Bangkok, New York, Lagos, Taipei, and Hong Kong. We meet in person every month to read, discuss, and pressure-test the latest blockchain papers, protocols, and technical ideas.
Learn more: Website · Summaries · Calendar
We create detailed, easy-to-understand summaries for each paper and have held 80+ sessions since June 2023, covering Account Abstraction, Parallel Chains, EIPs, the Bitcoin ecosystem, and AI x Crypto. We are ecosystem-agnostic, not for profit, and focused on projects with technical, product, or social innovation.