Click on "Deploy Server".
Wait a few minutes for the server to deploy. Once ready, it will show a "Started" state.
In the chat, type @ followed by the MCP server name and your instructions, e.g., "@mcp-server-quint run a simulation of bank.qnt to check the no_negatives invariant"
That's it! The server will respond to your query, and you can continue using it as needed.
Here is a step-by-step guide with screenshots.
MCP server for the Quint formal specification language. Wraps the Quint CLI to make formal verification accessible to any LLM-powered workflow.
npm i -g @informalsystems/quintclaude mcp add quint -- npx @dpdanpittman/mcp-server-quintThat's it. You now have 6 formal verification tools available in Claude Code.
Any MCP-compatible client can use this server over stdio:
npx @dpdanpittman/mcp-server-quint{ name: 'quint', command: 'node', args: ['/path/to/mcp-server-quint/index.js'] }Related MCP server: lu-mcp-server
quint_typecheckType-check a Quint specification. Provide either source (inline .qnt code) or file_path.
quint_runSimulate a Quint spec with random execution. Optionally check an invariant. Returns a counterexample trace if violated.
Parameter | Description |
| Spec to simulate |
| Init action name (default: "init") |
| Step action name (default: "step") |
| Invariant to check |
| Number of runs (default: 10000) |
| Steps per run (default: 20) |
| Random seed for reproducibility |
quint_testRun named test definitions (run statements). Optionally filter by match regex.
quint_verifyExhaustive model checking via Apalache. Checks ALL reachable states, not just random samples. Requires Java 17+ and Apalache.
quint_parseParse a spec and return the intermediate representation (IR) as JSON.
quint_docsQuick reference for Quint syntax. Topics: sets, maps, lists, actions, temporal, types, modules, testing, or all.
module bank {
var balances: str -> int
val ADDRS = Set("alice", "bob")
action init = balances' = ADDRS.mapBy(_ => 100)
action transfer(sender: str, receiver: str, amt: int): bool = all {
balances.get(sender) >= amt,
balances' = balances.set(sender, balances.get(sender) - amt)
.set(receiver, balances.get(receiver) + amt)
}
action step = {
nondet sender = ADDRS.oneOf()
nondet receiver = ADDRS.oneOf()
nondet amt = 1.to(balances.get(sender)).oneOf()
transfer(sender, receiver, amt)
}
val no_negatives = ADDRS.forall(a => balances.get(a) >= 0)
}Variable | Default | Description |
|
| Path to Quint CLI binary |
|
| CLI timeout in ms |
Quick reference for Quint syntax and built-in operators. Returns a curated cheat sheet for the requested topic. No CLI call needed.
Inputs: topic (required).
Parse a Quint spec and return the intermediate representation (IR) as JSON. Useful for inspecting the AST or checking for parse errors.
Inputs: source, file_path.
Simulate a Quint specification with random execution. Runs the state machine and optionally checks an invariant. Returns pass/fail and a counterexample trace if the invariant is violated.
Inputs: source, file_path, init, step, +4 more.
Run named test definitions (run statements) from a Quint spec. Returns pass/fail for each test with failure details.
Inputs: source, file_path, match.
Type-check a Quint specification. Returns success or type errors with locations. Provide either source code or a file path.
Inputs: source, file_path.
Exhaustive model checking of a Quint spec via Apalache (requires Java 17+). Slower than simulation but checks ALL reachable states. Returns pass or a counterexample trace. Falls back gracefully if Apalache is not installed.
Inputs: invariant (required), source, file_path, init, +2 more.
Recent tool additions, removals, and schema changes observed during successful MCP inspections.
Loading tool schema changelog…
Scored across 6 tools
Each tool has a clearly distinct purpose with no overlap: quint_docs provides syntax reference, quint_parse handles AST inspection, quint_run performs random simulation, quint_test executes named tests, quint_typecheck validates types, and quint_verify does exhaustive model checking. The descriptions clearly differentiate their specific functions within the Quint specification workflow.
All tools follow a perfect 'quint_verb' pattern consistently throughout, using lowercase with underscores. The verbs (docs, parse, run, test, typecheck, verify) are all action-oriented and descriptive, creating a highly predictable and readable naming convention.
Six tools is ideal for a Quint specification server, covering the complete lifecycle from documentation reference to parsing, testing, simulation, type checking, and verification. Each tool earns its place without redundancy, providing a well-scoped surface for working with Quint specifications.
The toolset provides comprehensive coverage for Quint specification workflows: documentation lookup, parsing, simulation, testing, type checking, and exhaustive verification. There are no obvious gaps—agents can perform the full CRUD-like lifecycle from inspection to validation and verification, with clear fallback behavior where appropriate.
AI-native programming language and toolchain for accountable, verifiable agent-driven development.
Architecture compiler for AI code. 11 tools, 92 actions, 872 Lean4 proofs, 100/100 self-cert.
Paid deterministic data-quality and execution-verification tools for AI agents.
Deterministic reasoning stack for AI agents: simulate, decide & compute, plus cross-domain tools.
