AI导哈

Quint形式验证服务器

用于Quint形式规范语言的MCP服务器，通过封装Quint CLI使形式验证可集成到任何LLM驱动的工作流中。

  • by dpdanpittman
  • JavaScript
  • 本地部署
  • 2 星标
  • 更新于
在 GitHub 查看 dpdanpittman/mcp-server-quint

使用说明

mcp服务器quint

MCP服务器 昆特 形式化规范语言。包装Quint CLI，使任何基于LLM的工作流都可以访问正式验证。

快速开始

1.安装Quint CLI

npm i -g @informalsystems/quint

2.添加到克劳德代码

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

就是这样。您现在在Claude Code中有6个正式的验证工具。

其他MCP客户端

任何兼容MCP的客户端都可以通过stdio使用此服务器：

npx @dpdanpittman/mcp-server-quint

使用超级网关（HTTP传输）

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

工具

quint_typecheck

类型检查Quint规格。提供其中之一 source （内联.qnt代码）或 file_path.

quint_run

通过随机执行模拟Quint规范。（可选）检查不变量。如果违反，则返回反例跟踪。

参数 说明
source / file_path 要模拟的规范
init 初始化操作名称（默认值：“Init”）
step 步骤动作名称（默认：“Step”）
invariant 不变检查
max_samples 运行次数（默认值：10000）
max_steps 每次运行的步数（默认值：20）
seed 随机种子可重复性

quint_test

运行命名测试定义(run 声明）。可选过滤条件 match 正则表达式。

quint_verify

通过Apalache进行详尽的模型检查。检查所有可到达的状态，而不仅仅是随机样本。需要Java 17+和 阿帕拉赫.

quint_parse

解析一个规范，并将中间表示（IR）作为JSON返回。

quint_docs

Quint语法快速参考。话题： sets, maps, lists, actions, temporal, types, modules, testing，或 all.

示例

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

环境变量

变量 默认值 描述
QUINT_CMD quint Quint CLI二进制文件的路径
QUINT_TIMEOUT 120000 CLI超时（毫秒）

许可证

PolyForm非商业版1.0.0

相关 MCP