Skip to main content
Glama
dpdanpittman

mcp-server-quint

by dpdanpittman

Server Configuration

Describes the environment variables required to run the server.

NameRequiredDescriptionDefault

No arguments

Instructions

Guidance the server publishes about itself, which clients place ahead of the tool catalog so the model reads it before choosing anything.

This server publishes no instructions, or was last inspected before Glama recorded them.

Capabilities

Features and capabilities supported by this server

Protocol revision2025-11-25

CapabilityDetails
tools
{
  "listChanged": true
}

Tools

Functions exposed to the LLM to take actions

NameDescription
quint_typecheckA

Type-check a Quint specification. Returns success or type errors with locations. Provide either source code or a file path.

quint_runA

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.

quint_testA

Run named test definitions (run statements) from a Quint spec. Returns pass/fail for each test with failure details.

quint_verifyA

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.

quint_parseA

Parse a Quint spec and return the intermediate representation (IR) as JSON. Useful for inspecting the AST or checking for parse errors.

quint_docsA

Quick reference for Quint syntax and built-in operators. Returns a curated cheat sheet for the requested topic. No CLI call needed.

Prompts

Interactive templates invoked by user choice

NameDescription

No prompts

Resources

Contextual data attached and managed by the client

NameDescription

No resources

TDQS

A4.1/5.0

Scored across 6 tools

Disambiguation5/5

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.

Naming Consistency5/5

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.

Tool Count5/5

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.

Completeness5/5

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.

Maintenance

ActivityInactive
ResponsivenessNo issues