quint_typecheck
Validate Quint specification type safety by analyzing source code or file paths to detect type errors with precise locations.
Instructions
Type-check a Quint specification. Returns success or type errors with locations. Provide either source code or a file path.
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 |
Implementation Reference
- index.js:146-164 (handler)The handler for the "quint_typecheck" MCP tool, which executes `runWithSource` with the "typecheck" command.
server.tool( "quint_typecheck", "Type-check a Quint specification. Returns success or type errors with locations. Provide either source code or a file path.", sourceSchema, async ({ source, file_path }) => { try { const result = await runWithSource(source, file_path, (f) => [ "typecheck", f, ]); return formatResult(result); } catch (err) { return { content: [{ type: "text", text: `Error: ${err.message}` }], isError: true, }; } }, );