Coding agents now write a lot of Rust. Just like us human devs, they work iteratively, checking their work as they go, correcting errors. And since we have to sit on our hands while they do the fun work, speed really matters.
Verus is a powerful toolchain that can be used to prove the correctness of Rust code. It checks Rust implementations against specs in the code. When it says a function meets its contract, that’s a general guarantee for every possible input, not just a sample like unit testing or PBT. See my colleague’s recent blog post for why you should prefer this stronger guarantee.
Strong guarantees are pretty desirable once the bots are writing all the code. But verification as a step in the average SDLC has historically been a tough sell. With agents doing all the code gen, the work of getting verification guarantees into your codebase gets way easier. But like with a lot of things in agentic dev, the loop can get real slow and inefficient. If you don’t like the speed of the Rust compiler, you’re not going to love the additional time code verification via Verus adds. But you should verify your code. So, I built the tool that makes that experience easier.
Today I’m releasing Sail, an efficient verification server with support for Verus.
Origin
I spent the past year building a programming language called Chelis with some colleagues. It’s built for coding agents as its primary authors and has verification built into the language at the compiler level.. I repeatedly saw that agents use proofs well, writing specs and iterating against a verifier much as they iterate against a compiler. But feedback needs to return quickly and have useful actions, otherwise the whole process starts to grind.
The solvers themselves are pretty great. Z3, cvc5 and friends, truly all impressive and pretty well engineered. They’re not inherently leaving a lot of perf on the table at their level. But there’s a lot more in the outer loop that starts to add up: latency, caching, costs of non-determinism, and so on. When you look at what the agents really need, there’s a lot of missing functionality, so I decided to fill in those gaps.
As much as I think Chelis is a good guide to the future of software development, I wanted to help people writing mainstream code today, so this first version exclusively targets Rust code and uses the awesome Verus library (with a few tweaks to help maximize perf).
Verus Perf
Verus is great, but it’s not focused on performance. It checks each function against the specifications of the functions it calls rather than their bodies. That makes verification work modular: change one function, and most of the proof effort for the rest of the crate is still valid. Unfortunately, stock Verus throws that work away and redoes everything on every run, so a one-line edit costs about as much as verifying from scratch. Undoing the edit costs the same again.
This adds up to a lot of wasted time for a coding agent that edits, fails, fixes and backtracks all day.
Sail Usage
sail verify is a drop-in replacement for cargo verus verify. It takes the same arguments, prints the same output, and gives the same verdicts. Behind that interface, I didnt’ change anything I didn’t have to.
But I do a lot to improve the perf story. Solver answers are cached across edits. Proofs of untouched code are reused. When you undo an edit, the earlier proof is restored. When nothing has changed at all, the previous result is replayed in a few hundredths of a second. All of these improvements really start to add up.
Here’s what that looks like on real Verus projects, measured on Linux against stock Verus:
-
Fail, then fix. A failing edit on Anvil, a verified Kubernetes controller, comes back in 27 seconds instead of 146. That failing state is where an agent spends much of its time.
-
Undo. Reverting an edit on Vest, a verified parser library, takes 1.1 seconds instead of 39.
-
Everyday edits. One-line edits are 1.2 to 2.5 times faster on every project I tested, on Linux and macOS.
The full measurements, including the cases where Sail is slower than stock, are in the performance notes.
Same, but Faster
A faster verifier is worthless if it ever gives you the wrong answer, so I have to hold to parity for the solution verdicts. In its default mode, Sail produces the same per-function verdicts, diagnostics and exit codes as stock Verus (on the pinned version of Z3).
Sail ships its own build of Verus, a fork that makes the verifier deterministic and lets Sail reuse work safely. You don’t need a separate Verus install, and your existing one is left alone. Switching back is as simple as running cargo verus verify again.
Users
Sail is for anyone verifying Rust with Verus, and most of all for anyone having agents grind on verification. For agents and other programs, I expose JSON and MCP interfaces to verification, background jobs, failure explanations and proof-repair checks. Registering it with Claude Code is one command:
claude mcp add --transport stdio sail -- sail mcpNext
Faster verification with Verus is the first delivery of a longer project. My bigger goal is making solvers and provers work efficiently and ergonomically for agents. Some really exciting work in the pipeline that will be landing in open source soon.
Try it
Sail 0.1.0 runs on Linux x86-64 and Apple-silicon macOS. From a checkout of the repository:
python3 scripts/install.py --version 0.1.0 --install-toolchainThen, in any Verus project, run sail verify wherever you’d run cargo verus verify. To start fresh:
sail new --lib demo
cd demo
sail verifyAnything not look right? Please open an issue.
Happy sailing!