MCP 服务器

mcp-server-quint

Integrates the Quint formal specification language into LLM workflows for accessible formal verification. It provides tools for type-checking, random simulation, exhaustive model checking, and syntax documentation.

README

mcp-server-quint

MCP server for the Quint formal specification language. Wraps the Quint CLI to make formal verification accessible to any LLM-powered workflow.

Quick Start

1. Install Quint CLI

npm i -g @informalsystems/quint

2. Add to Claude Code

claude mcp add quint -- npx @dpdanpittman/mcp-server-quint

That's it. You now have 6 formal verification tools available in Claude Code.

Other MCP Clients

Any MCP-compatible client can use this server over stdio:

npx @dpdanpittman/mcp-server-quint

With Supergateway (HTTP transport)

{ name: 'quint', command: 'node', args: ['/path/to/mcp-server-quint/index.js'] }

Tools

`quint_typecheck`

Type-check a Quint specification. Provide either source (inline .qnt code) or file_path.

`quint_run`

Simulate a Quint spec with random execution. Optionally check an invariant. Returns a counterexample trace if violated.

Parameter	Description
`source` / `file_path`	Spec to simulate
`init`	Init action name (default: "init")
`step`	Step action name (default: "step")
`invariant`	Invariant to check
`max_samples`	Number of runs (default: 10000)
`max_steps`	Steps per run (default: 20)
`seed`	Random seed for reproducibility

`quint_test`

Run named test definitions (run statements). Optionally filter by match regex.

`quint_verify`

Exhaustive model checking via Apalache. Checks ALL reachable states, not just random samples. Requires Java 17+ and Apalache.

`quint_parse`

Parse a spec and return the intermediate representation (IR) as JSON.

`quint_docs`

Quick reference for Quint syntax. Topics: sets, maps, lists, actions, temporal, types, modules, testing, or all.

Example

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)
}