quint_verify
Verify invariants in Quint specifications through exhaustive model checking with Apalache. Checks all reachable states to validate system properties.
Instructions
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.
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| source | No | Quint specification source code (.qnt content) | |
| file_path | No | Path to a .qnt file on disk | |
| init | No | Init action name (default: "init") | |
| step | No | Step action name (default: "step") | |
| invariant | Yes | Invariant to verify (required) | |
| max_steps | No | Max steps for bounded model checking (default: 10) |
Implementation Reference
- index.js:274-310 (handler)The handler logic for the 'quint_verify' tool, which uses 'runWithSource' to execute the 'quint verify' command with the provided parameters.
async ({ source, file_path, init, step, invariant, max_steps }) => { try { const result = await runWithSource(source, file_path, (f) => { const args = ["verify"]; if (init) args.push(`--init=${init}`); if (step) args.push(`--step=${step}`); args.push(`--invariant=${invariant}`); if (max_steps != null) args.push(`--max-steps=${max_steps}`); args.push(f); return args; }); // Add hint if Apalache is missing const output = [result.stdout, result.stderr] .filter(Boolean) .join("\n") .trim(); if ( result.exitCode !== 0 && (output.includes("Apalache") || output.includes("java") || output.includes("JAVA_HOME")) ) { return { content: [ { type: "text", text: output + "\n\nHint: quint verify requires Apalache (Java 17+). Install Java and Apalache, or use quint_run for simulation-based checking.", }, ], isError: true, }; } return formatResult(result); - index.js:261-273 (registration)The registration of the 'quint_verify' tool, including its schema definition.
server.tool( "quint_verify", "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.", { ...sourceSchema, init: z.string().optional().describe('Init action name (default: "init")'), step: z.string().optional().describe('Step action name (default: "step")'), invariant: z.string().describe("Invariant to verify (required)"), max_steps: z .number() .optional() .describe("Max steps for bounded model checking (default: 10)"), },