# Sail

Faster Verus checks and reusable Z3 results, with MCP tools for coding agents.

Author: Jeffrey Kent
Canonical: https://jeffreykent.dev/software/sail/
Published: 2026-11-01
Updated: 2026-11-01
Source: https://github.com/Chelis-Lang/sail
Source revision: b7666c37d305efdb2a3ed34af6f3dd41d9539495

Sail is an open-source replacement for `cargo verus verify` that makes repeated verification faster. It caches Z3 answers, keeps proofs for unchanged targets and restores earlier proofs when you undo an edit.

In the [release benchmarks](https://github.com/Chelis-Lang/sail/blob/v0.1.0/docs/performance.md), one-line edits verified 1.2 to 2.5 times faster across the tested projects. On Linux, a failing Anvil edit returned in 27 seconds instead of 146, and a Vest revert took 1.1 seconds instead of 39.

Try `sail verify` in place of `cargo verus verify`. Sail builds in its own target directory and leaves your existing Verus installation alone.

Coding agents get MCP tools for verification, failure explanations and repair checks. For SMT work outside Rust, Sail also provides bundled Z3 execution with a persistent result cache, from the CLI or a shared service.