Add Sail’s MCP server 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 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.