Writing
- Proof languages compared: Lean vs Dafny vs Verus vs Rocq (2026)Lean 4, Rocq, Isabelle, Agda, Idris 2, F*, Dafny, Verus, SPARK, Why3, Liquid Haskell, Bend 2, TLA+, Alloy and P compared on what you prove, how much is automatic, what code they produce, maintenance and how well AI agents write proofs in them. Short answer: Dafny or Verus for proving your own code, Lean for deep proofs, TLA+ or P for distributed designs.Article
- What is formal verification? Proofs explained for developersFormal verification proves code meets its spec for every input, and a small checker confirms each step, so you don't have to trust whoever (or whatever) wrote it. A runnable Lean example, proofs vs tests, the kinds of tool, costs, production users and what AI agents manage today.Article
