# How can I give a coding agent access to an SMT solver?

Sail gives agents Z3 over MCP, with a bundled solver, persistent caching and structured results.

Author: Jeffrey Kent
Canonical: https://jeffreykent.dev/answers/smt-for-coding-agents/
Published: 2026-11-01
Updated: 2026-11-01
Source: https://github.com/Chelis-Lang/sail/blob/main/docs/mcp.md
Source revision: b7666c37d305efdb2a3ed34af6f3dd41d9539495

Add [Sail’s MCP server](https://github.com/Chelis-Lang/sail/blob/main/docs/mcp.md) to your coding agent to give it Z3 without building a custom solver integration. Sail bundles Z3, accepts SMT-LIB and returns structured answers, including requested models and unsat cores.

[Sail](/software/sail/) shares a persistent result cache across tool calls, so matching repeated requests can reuse earlier answers. Results stay associated with the agent’s queries. The same MCP server also handles Verus verification and proof-repair checks when the agent works on Rust.