Learn formal verification
Curated resources for practitioners exploring verified software. Books, courses, tools, and communities — organized by where you are in the journey.
Getting Started with Lean 4
Theorem Proving in Lean 4
The official textbook. Covers logic, tactics, and dependent types from scratch.
Functional Programming in Lean
David Christiansen's guide to Lean as a programming language, not just a proof assistant.
Mathematics in Lean
Tutorial on formalizing mathematics using Lean and Mathlib. Best for math-inclined learners.
The Mechanics of Proof
Heather Macbeth's undergraduate-level textbook teaching proof techniques through Lean 4.
Lean 4 Web Playground
Try Lean in your browser. No installation needed.
Courses
Key Articles
AI Will Make Formal Verification Mainstream — Martin Kleppmann
The clearest argument for why AI changes the economics of verification. December 2025.
Lean 4: How the Theorem Prover Works — VentureBeat
Accessible overview of why Lean 4 is becoming the competitive edge in AI systems.
Formal Verification, Casually Explained — Andrew Helwer
Gentle introduction to formal verification concepts for software engineers.
Formally Verified Software in the Real World — CACM
Survey of verified software deployed in production, including seL4 and CompCert.
Tools & Infrastructure
Lean 4
The proof assistant and programming language. Start here.
Mathlib
Community math library for Lean 4. 210K+ formalized theorems and growing.
LeanDojo
Infrastructure for AI-driven theorem proving. Datasets, benchmarks, and tools for training proof agents.
Leanstral
Mistral's open-source Lean 4 code agent. 6B active params, Apache 2.0.
DeepSeek-Prover-V2
Open-weight theorem prover. 88.9% on MiniF2F-test. Available in 7B and 671B sizes.
AWS Cedar
Formally verified authorization policy engine. Open-source, production-grade.
Communities
Know a resource that should be here? Let us know.