mcp-server-quint

Instructions

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