Matsakis Names Four Rust Verifiers for Agents, and Their READMEs Cover Different Ground

Niko Matsakis argued on Oct. 14 that Rust suits agent-written code and could be made to suit it better, and he named four proof tools as the way to get there: Verus, Creusot, Aeneas and Kani. His post on the baby steps blog, a companion to a talk at REBASE, part of SPLASH, says agents could optimise code while a prover confirms it still computes the right answer.

The post does not compare the four. Their own repositories do, and the differences decide what an agent could safely be told to do.

What Matsakis proposes

Matsakis's post splits a "software factory" into design, construction and optimization, and says optimization is furthest along. He proposes a loop of code, benchmark, profile, agent, pull request, and back to code. He cites the dial9 profiler as something network-service builders use so agents can find async pitfalls such as long polls.

On reliability he is blunt about tests. Agents often pass early tests and then produce bizarre bugs, he writes, and he cites Dijkstra's line that testing shows the presence of bugs, not their absence. His north star is "no more unsafe code": not removing the keyword, but proving that unsafe code cannot cause undefined behavior.

Two claims in the post are secondhand. Matsakis attributes to David Tolnay the observation that Meta engineers wrote more first-party Rust in 2026 than in the previous nine years combined, and to Greg Brockman the claim that if Rust code compiles it is roughly correct. We found no original for the Tolnay figure in a search, so treat it as Matsakis's report of it.

The four tools side by side

Tool	Licence	Stars	Backend or method
Kani	MIT and Apache-2.0	3.5k	Model checker
Verus	Not named on page	3.3k	Solvers, a Rust subset
Creusot	LGPL-2.1	1.9k	Why3 platform
Aeneas	Apache-2.0	1.0k	F*, Coq, HOL4, Lean

1. Kani3.5 thousand stars
2. Verus3.3 thousand stars
3. Creusot1.9 thousand stars
4. Aeneas1 thousand stars

Source: Each project's GitHub page, accessed 2026-10-15

Kani checks for crashes and undefined behavior

Kani calls itself "a bit-precise model checker for Rust" and "automatically checks panics (e.g. unwrap() on None), arithmetic overflows." It also checks for many kinds of undefined behavior, which the page presents as useful for unsafe blocks. That is closest to the panic-freedom starting point Matsakis names. The README lists no limitations section.

Verus proves a specification, on a subset of Rust

Verus takes a specification the developer writes and "statically checks that the executable Rust code will always satisfy the specifications for all possible executions." Its page warns that it is "under active development," that features may be broken or missing, and that it "currently supports a subset of Rust." Its releases section was empty when we read it.

Creusot and Aeneas hand the proof to other systems

Creusot is "a deductive verifier" that translates Rust into Coma, an intermediate language of the Why3 platform, and then asks Why3 to discharge the verification conditions semi-automatically. Its licence is LGPL-2.1, the only copyleft entry in the table.

Aeneas translates Rust's MIR into a pure lambda calculus for proof assistants, working with a tool called Charon. "Our most mature backends are Lean and HOL4," the README says. Its listed limits are the ones an agent would hit first: returning from nested loops and breaking to outer loops are unsupported, as are generic types instantiated with mutable references. Unsafe code and concurrency are named as limits that separation-logic work is expected to lift.

What this means for an agent in the loop

Matsakis ties the borrow checker to Verus: because uniqueness is guaranteed by the type system, the SMT solver has an easier job. The Verus page does not discuss ownership, so that claim is his and not the project's.

The gap between the two sources is the practical finding. An agent told to "prove it" would need a tool whose supported Rust subset covers the code it just wrote. Kani covers panics and undefined behavior today. Aeneas excludes unsafe code and concurrency. Verus covers a subset and says so.

Two earlier stories here show the same pressure on code review: a kernel patch series written with Claude Code and a benchmark that ranks coding agents by how much code their fixes add. Matsakis gave no date for any language change, and none of the four repositories reported a release when we read them on Oct. 15.