#FormalMethods

Hillel @hillelogram

Okay, let's do this. Isabelle, Lean, and Rocq (formerly Coq*) are theorem provers. They are meant to prove mathematical theorems. We use them for formal verification by either 1) translating a program to the theorem prover (risking a translation error) or 2) using a language built into the theorem prover that extracts into a working binary. Fizzbee, TLA+, Spin, Alloy, Quint, and P are specification languages. They are meant for checking high-level blueprints of programs. After checking the blueprint, you still need to make sure your program matches it, which is a hard problem. Specification languages differ in what they make easy to express. P, Spin, and Fizzbee are designed to be closer to the code implementations. P looks like interacting state machines, Spin looks like C with CSP, Fizzbee looks like a dialect of Python. It's easier to use a codelike specification language and refine it to code, but you can't do as much with it. Alloy, TLA+, and Quint are more abstract. Alloy looks like a bunch of algebraic relationships, TLA+ is a much of logical formula, and Quint is a programmer-oriented (and statically typed) condensation of TLA+. Abstract modeling languages are harder to get started with and harder to represent things, but you can represent a wider class of systems with them. I believe UPPAAL is a specification language for realtime systems. This is a field I have no experience in. It seems a graphical language, though, which would make LLM-assistance difficult. Dafny is a verifiable programming language. It has regular programming language features, but also a bunch of features to express and prove properties of the program. It uses SMT solvers to actually prove the properties, meaning you don't need to learn a proof language (though you need to learn to cajole the solver). Dafny is probably the easiest thing on your list to get started with, but also the least likely to meet any weirder needs you might have. I don't know what Ivy is but some cursory Kagiing suggests it falls in the specification language category. Some other things @spin_lock_init didn't mention: - Other theorem provers: Agda, Metamath - Other abstract specification languages: mcrl2, NuXMV, Event-B - Other verifiable programming languages: Idris, F*, Whiley - There's also using a verifiable subset of a language, like Verus for Rust or SPARK for Ada. So, what you need to pick depends on what you want to do. You'll get the maximum power with a theorem prover. Lean is the de facto language for vibeproving, but Anthropic recently published a post about vibeproving in Rocq so YMMV. If you want to make abstract models of software systems, go for a specification language. Which you choose depends on a lot of factors. If your system can be represented as lots of simple communicating state machines over a network, try P. Spin, I believe, is close to simple C/Go with a network and channels. I have never used Fizzbee. Alloy is good for domain modeling, but struggles with really complicated temporal actions, nested data structures, and largish numbers. Also AIs aren't to good at it (last I checked, in March). Runs fast and makes good visualizations though. TLA+ and Quint are for modeling complex temporal systems. I'm partial to TLA+ but know a lot of people who say Quint is easier to get into. Note P, Fizzbee, and Quint all claim to have features for testing a codebase against a spec. I can't vouch for any of them, though. None of the languages I mentioned (except maybe NuXMV?) are particularly good at modeling sequential, deterministic algorithms. Use Dafny if you need to just write a verified program and don't care which language it's in. I don't think other verifiable programming languages are as user-friendly for the time being. Consider a verified subset if you already know a language and want to just augment it with more correctness. You may need other, more exotic tools depending on your particular needs. Regardless of the above advice, don't be afraid to use the wrong tool for the job. If you vibe well with a language, and you achieve good LLM-sympathy with it, you'll be able to go farther than using a "right tool" you don't like.

Alex Lavaee @alexlavaee

We spent fifty years making proofs impossible to fake. Then we let the coding agent pick what to prove. A research paper this month put a number on it.* AI wrote the formal spec, AI wrote the proof, the verifier accepted both. Then humans read the specs. Close to 60% proved something other than what the author meant. Not wrong proofs. Wrong specs. The verifier was right every time. That's the problem. Left to choose, the agent picks properties that are easy to prove and say nothing about the program, and the checker can't tell a useless theorem from a useful one. I'm calling it vibe verification: the agent writes the spec and the proof, the checker goes green, nobody reads the spec. This applies to Verus, Lean, Bend, TLA+, Dafny, [insert favorite formal language here]. Here's an example of an agent failing at something that feels too simple to fail: Ask for a verified sort. It writes a spec that says "the output is sorted" and proves it. What the spec never says is that the output has the same elements as the input, so a function that returns an empty list satisfies it, and the verifier accepts the proof. Trivially satisfiable specs are the default failure, not an edge case. Here's a formula that actually works. Don't say "formally verify the codebase." Say "show that [property] holds in [component]." A property is a precondition (true going in), a postcondition (true coming out), or an invariant (stays true the whole time). For example, "A session token is never accepted after the logout that revoked it" is a good invariant. The bottleneck is moving from code review to intent review, and the spec is where intent lives. So: read the spec before the code. Write 3 inputs it must accept and 3 it must reject. Treat a model-written spec with utmost paranoia and rely on your judgement as an engineer. Formal verification for software doesn't automatically create trust, it moves it, from the code to the spec. If a human didn't read the spec, you didn't verify anything. You vibe-verified it. Follow me for more on verification and agentic engineering. * Wang, Jiang, Liu et al., "VerusEval: Evaluating LLM-Generated Verus Specifications Beyond Verifier Acceptance", Shenzhen University, arXiv 2610.26464, October 2026

Axiom @axiommathai

The largest math proof in human history is now computer-verified. Today, Axiom announces a complete Lean auto-formalization of the Classification of Finite Simple Groups, the "periodic table of symmetry." About 15,000 pages, built by over 100 mathematicians across generations.

Thomas Coratger @tcoratger

This weekend we launched EthLib, a Lean4 library for Ethereum! The goal is to bring Ethereum's primitives, specifications and theorems into one place, building a shared foundation for formally specifying and proving things about Ethereum.

Claudio @menghi_claudio

FM Tutorial series Date: June 17, 2022 Speaker: Dr Tim Nelson (Brown University, US) Title: Building Formal Methods Classes for Everybody Further information and zoom link

Michael Bar-Sinai @michbarsinai

@hillelogram Great roundup! May I also add Behavioral Programming (e.g. Provengo, JS-based executable specification language. Can test against a spec, implement correct-by-construction control logic, and visualize & verify algos. Very easy to learn if you know JS.