| Nov 7, 2026 | Veil 2.0 is out! It is the most feature-complete library for multi-modal foundational verification of distributed protocols in Lean. The new release features: - Lace, a verified, blazing-fast explicit-state model checker for safety (2–20x faster than TLA+/TLC on equivalent models)
- Lasso, a fast verified model checker for LTL-style liveness specifications (which also beats TLC)
- A dedicated interactive proof mode for LTL specifications
- An LLM skill for translating TLA+ specifications to Veil, together with nearly 40 models ported from TLA+ (including Paxos, EPaxos, NOPaxos, and Raft)
- A PlusCal-style DSL for customisable, program-style definitions of your distributed protocols
Check it out on GitHub or try it in your browser! |
| Nov 6, 2026 | &Truth got featured in The New York Times and Wired! |
| Oct 29, 2026 | &Truth, the company I co-founded, is out of stealth! Together with a team I’m immensely proud to be part of, our ambition is to specify and prove all the world’s software correct and secure. Join us! |
| Oct 18, 2026 | New post on Proofs and Intuitions: The Vermilion Experiment: Implementing a Lean Backend for Verus. |
| Sep 28, 2026 | A two-weekend fun project: Vermilion, an experimental Lean 4 backend for the Verus verifier for Rust. Verification conditions are readable Lean theorems, provable with an SMT solver, Lean’s grind, Mathlib lemmas, by hand, or by your favourite AI system. |
| Sep 18, 2026 | We have released a new version of Velvet, our foundational multi-modal verifier for imperative programs in Lean, with a number of new features. It now has a new web site! |
| Aug 15, 2026 | Four papers from VERSE lab will appear at OOPSLA 2026: |
| Aug 14, 2026 | New post on Proofs and Intuitions: When the Hard Part Stops Being Hard, on how AI-assisted formal verification is reshaping programming-language research, letting individual researchers do in weeks what used to take months. |