Back to Posts
Link
Lean Squad: Exploring Automated Software Verification with Near-Zero Human Labour
https://dsyme.net/2026/04/20/lean-squad-automated-software-verification-with-near-zero-human-labour/
What if formal verification could be fully automated — from researching the codebase, to writing specifications, to proving theorems in Lean 4 — all with near-zero human involvement? Lean Squad is a GitHub Agentic Workflow that does exactly this. Applied to three real-world codebases, it produced over 1,200 machine-checked theorems and found real bugs in a drone autopilot.
Read more on the blog of our Principal Researcher Don Syme.