Proof
Model checkers and verifiers, now that an agent can draft the proof.
Writing a TLA+ spec or a Dafny proof was a specialist's job for decades. A coding agent will draft one in minutes, and the checker settles whether it holds. Rule 16 calls this boiling the lake.
Show tools for
28 tools
Model checkers, verifiers and contracts
Start here
CBMC
Bounded model checker for C and C++ that finds assertion failures and memory errors.
A harness reads like a test yet covers every input within a bound, and AWS uses it on core libraries.
Start here
Checker Framework
Pluggable type checkers for Java that enforce nullness, resource and custom rules at compile time.
Violations fail the build at compile time, so an agent has no runtime path around them.
Start here
Dafny
Verification-aware language where a solver proves contracts and the code compiles to several target languages.
Specs and code live together and the proof has to pass, which suits an agent that retries until the verifier is satisfied.
Start here
Gobra
Verifier for Go programs using contract annotations, built on Viper.
One of very few ways to prove Go code, and the SCION network stack uses it.
Start here
icontract
Design by contract for Python with preconditions, postconditions and invariants as decorators.
Pre- and postconditions become runtime guardrails, and icontract-hypothesis can generate tests from them.
Start here
Kani
Bit-precise model checker for Rust that proves harnesses hold for all inputs within bounds.
A harness reads like a test yet proves the property, so unsafe Rust gets checked without learning a proof language.
Start here
Liquid Haskell
Adds refinement types to Haskell so the compiler proves properties like non-empty lists or bounds.
Contracts live in types, so the compiler checks them on every build.
Start here
SPARK (GNATprove)
Ada subset with contracts that the GNATprove tool proves free of runtime errors.
The mature example of contracts enforced by proof in production, notably in aerospace and rail.
Start here
Stainless
Verifier for a functional subset of Scala that proves contracts and termination.
Brings proof-backed contracts to Scala for teams that need guarantees on core logic.
Start here
Stateright
Model checker for distributed protocols written in Rust, which can also run the checked actors as real code.
Bridges a protocol model and a running implementation, so the checked design is the shipped code.
Start here
TLA+ (TLC and Toolbox)
Specification language and model checker for describing and checking concurrent and distributed designs.
A TLA+ spec is a contract for a protocol that TLC checks exhaustively, and agents now draft them with some success.
-
Alloy
Lightweight modeling language that finds counterexamples to claims about data models and rules.
A quick way to find holes in a data model or permission design before agents build on it.
-
Apalache
Symbolic model checker for TLA+ that uses an SMT solver on large or infinite state spaces.
Handles specs with big integers and parameters that stall TLC, giving faster feedback inside an agent loop.
-
Concuerror
Concuerror finds concurrency errors in Erlang programs.
It helps catch concurrency bugs that only appear in rare schedules.
-
Creusot
Deductive verifier for Rust that translates programs to Why3 for proving.
Gives stronger guarantees than bounded checks for algorithmic Rust and asks for more proof effort.
-
deal
Design by contract for Python with runtime checks, linting and automatic test generation.
Contracts can also be proven with Z3 and run under pytest.
-
F*
Proof-oriented language that extracts verified code to OCaml, F# or C.
Verified crypto and parsers written in it ship in real products, and researchers are testing agents on it.
-
Frama-C
Analysis platform for C that checks ACSL contract annotations with proof plugins.
Contract comments in C can be proven with the WP plugin, which suits embedded and safety-critical code.
-
GraphWalker
Model-based testing tool that walks a graph model of the system to generate test paths.
A graph of states and transitions gives the team a model to generate paths from and explicit coverage targets.
-
Lean 4
Programming language and proof assistant where a small trusted kernel checks every proof.
A machine-checked proof is a hard gate an agent cannot talk past, and AI provers target it.
-
Nagini
Static verifier for statically typed Python using contract annotations, built on Viper.
A rare prover for Python, though research-grade and limited to a subset.
-
OpenJML
Checks Java code against JML contract annotations by static verification and runtime checks.
Gives Java a path to proven contracts, though use is mostly academic.
-
P language
State-machine language for modeling distributed systems, used by AWS teams on S3, DynamoDB and EC2.
The repo ships PeasyAI, an MCP tool that lets Claude Code and Cursor write and fix P models.
-
Quint
Executable specification language with TypeScript-like syntax that runs on the Apalache checker.
Developers and agents both read the syntax easily, and the simulator and REPL give quick checks of a spec.
-
Rocq (Coq)
Proof assistant, renamed from Coq, for proving programs and mathematical statements correct.
Verified compilers and kernels are built on it, and its proofs are checked mechanically.
-
Specula
LLM framework that derives TLA+ specs from source code and validates them against real traces.
Shows the loop IMP wants: an agent drafts the spec from code, then trace checking ties it to behavior.
-
Verus
Verifier for Rust that proves code meets specs written in Rust syntax, using an SMT solver.
The main target for LLM proof-writing research, since specs stay in Rust and the solver checks every step.
-
XState + @xstate/test
State machine library whose models can generate test paths that drive the real UI or service.
The state machine is the contract, and generated paths test the implementation against it.
Nothing in this section is built for the stacks you picked, and nothing here works with any language. Pick another stack, or .
Gone quiet 1
These tools are archived or shut down, or nobody has released or committed to them in two years. Some still work fine. Read the note before you adopt one.
-
Prusti
Rust verifier built on Viper that checks contracts written as attributes.
Attribute-style pre- and postconditions read like design by contract and are easy for an agent to write.
Little activity since March 2024.
Missing a tool that belongs here? Suggest it.
Every tool here was checked against its GitHub repository or its own site on 6 October 2026. Stars and dates come from GitHub on that day.