C*：开发与证明一体化

用 cstar_mcp 进行 AI 辅助验证

EN | 中文

前两节介绍了证明中两部分工作的自动化：策略负责匹配并消去空间资源，SMT 求解器负责解决剩余的纯目标。但在编写第一个证明块之前，数据采用什么逻辑模型、如何定义谓词族、选用什么循环不变式、用哪条引理填补证明的缺口，都无法由它们决定。此前在本教程中，这些判断都由人在 VSCode 中阅读符号状态后作出。 cstar_mcpcstar_mcp 将同样的工作流交给 AI 助手。它通过 MCP（Model Context Protocol，即 AI 助手调用外部工具的接口）向助手提供验证器的功能，让助手能够查看某一行的符号状态、搜索定理数据库、编辑证明块，再次检查验证结果。

配置

服务器随工具链一起发布，位于 ~/.cstar/bin/cstar_mcp~/.cstar/bin/cstar_mcp。无论使用哪种助手，都可以按以下参数在 MCP 客户端中注册服务器：

  • 传输方式：标准输入输出（由客户端启动的本地进程）；
  • 命令：二进制文件的绝对路径 /Users/you/.cstar/bin/cstar_mcp/Users/you/.cstar/bin/cstar_mcp，因为配置不是由 shell 读取的，~~ 不会被展开；
  • 参数：无；
  • 环境变量：无需设置；可通过 CSTAR_MCP_MAX_STACKSCSTAR_MCP_MAX_STACKS 提高常驻文件的数量上限（默认为三个）。

工具

连接到服务器的助手可以看到六个工具。

工具 作用
cstar_showlspcstar_showlsp {path, line}{path, line}：某一源码行处的验证状态，即该行执行之后的状态。在函数内部查询时，回复包含 symbolic_statesymbolic_state 与作用域内的幽灵变量；在文件作用域（从函数的右花括号起），回复包含截至该行累积的 vcvc。lines: [...]lines: [...] 一次查询同一文件的多行，scopesscopes 则限制幽灵变量的转储内容。
search_theoremssearch_theorems {pattern, limit?}{pattern, limit?}：用正则表达式搜索具名 HOL Light 定理（包括定理语句）；名字完全匹配的结果排在最前
search_conversionssearch_conversions {pattern, limit?}{pattern, limit?}：以同样的方式搜索具名变换
cstar_helpcstar_help {topic?}{topic?}：证明工作流指南，或其中的某个参考主题（syntaxsyntax、contractscontracts、memorymemory、predicatespredicates、loopsloops、bitopsbitops、aritharith、projectproject、techniquetechnique、operationsoperations、apiapi、errorserrors）
cstar_killlspcstar_killlsp {path?}{path?}：发生内部故障后，终止某个文件或所有文件的证明器与常驻守护进程
cstar_interruptcstar_interrupt {}{}：中止一个无响应的证明器请求；证明器本身继续运行

cstar_showlspcstar_showlsp 是 Show Symbolic StateShow Symbolic State 对应的 MCP 工具，源码位置的查询规则与 VSCode 命令相同：查询函数内的行，显示该行执行后的状态；查询文件作用域中的行，返回截至该行收集到的验证报告。因此，只有查询文件真正的最后一行，且返回的 verification_conditionsverification_conditions、axiomsaxioms 与 strategiesstrategies 都为空时，文件才算通过验证。首次查询一个文件时比较慢，因为需要启动该文件的证明器并构建常驻守护进程；之后查询同一文件就能很快返回，守护进程也会自动处理文件的修改。默认最多有三个文件同时保持常驻（可通过环境变量 CSTAR_MCP_MAX_STACKSCSTAR_MCP_MAX_STACKS 提高上限），每个文件都有独立的证明器，因此在这些文件之间切换没有代价。查询第四个文件时，会淘汰最久未使用的那个，并在回复的 notenote 中说明。

助手的工作流

cstar_helpcstar_help 提供的指南明确列出了工作流，与本教程此前手工完成的流程相同：

  1. 先设计数据的逻辑模型、谓词族、函数契约，以及折叠与展开引理，然后再编写代码与证明块；对于递归函数，可将结果的大小或高度等性质写入后置条件，以便在递归调用后直接使用这些性质；
  2. 每写完一个函数，就查询它的右花括号所在行，验证该函数；
  3. 验证失败时，查询证明块前后的可执行行，阅读符号状态；
  4. 搜索定理与变换数据库，寻找能填补证明缺口的定理或变换；
  5. 编辑证明块后再次查询，此时文件已预热；
  6. 最后查询文件的最后一行，返回的三个列表都必须为空。

一次关于 twicetwice 的会话

将C* 中的前向证明中的 twicetwice 函数保存为独立项目中的 twice.ctwice.c；第 12 行是 int r = a + b;int r = a + b;，第 27 行是函数的右花括号。下面展示三次调用中助手发出的请求和服务器的回复（较长的值已截短；路径可使用绝对路径，也可相对于服务器启动时所在的目录）：

cstar_showlsp {"path": "twice.c", "line": 12, "scopes": "none"}
{
  "flag": true,
  "lsp": {
    "function": "twice",
    "line": 12,
    "symbolic_state": "fact (0i <= n__pre) ** fact (n__pre <= 100i) **
      data_at r__addr Tint ((n__pre + 1i) + n__pre - 1i) **
      data_at b__addr Tint (n__pre - 1i) **
      data_at a__addr Tint (n__pre + 1i) **
      data_at n__addr Tint n__pre",
    …
  }
}
cstar_showlsp {"path": "twice.c", "line": 12, "scopes": "none"}
{
  "flag": true,
  "lsp": {
    "function": "twice",
    "line": 12,
    "symbolic_state": "fact (0i <= n__pre) ** fact (n__pre <= 100i) **
      data_at r__addr Tint ((n__pre + 1i) + n__pre - 1i) **
      data_at b__addr Tint (n__pre - 1i) **
      data_at a__addr Tint (n__pre + 1i) **
      data_at n__addr Tint n__pre",
    …
  }
}

这与 VSCode 面板在该行显示的状态相同，rr 所在的单元保存着尚未化简的和。查询最后一行时，返回的是验证报告。由于两个证明块都已写好，三个列表都为空：

cstar_showlsp {"path": "twice.c", "line": 27, "scopes": "none"}
{
  "flag": true,
  "lsp": {
    "line": 27,
    "vc": { "axioms": [], "strategies": [], "verification_conditions": [] },
    …
  }
}
cstar_showlsp {"path": "twice.c", "line": 27, "scopes": "none"}
{
  "flag": true,
  "lsp": {
    "line": 27,
    "vc": { "axioms": [], "strategies": [], "verification_conditions": [] },
    …
  }
}

搜索结果包含定理名字与定理语句，使用打印器的记号：

search_theorems {"pattern": "REVERSE_APPEND", "limit": 2}
[
  {
    "name": "REVERSE_APPEND",
    "statement": "|- forall l m. REVERSE (l ++ m) == REVERSE m ++ REVERSE l"
  }
]
search_theorems {"pattern": "REVERSE_APPEND", "limit": 2}
[
  {
    "name": "REVERSE_APPEND",
    "statement": "|- forall l m. REVERSE (l ++ m) == REVERSE m ++ REVERSE l"
  }
]

查询失败时，回复包含 flag: falseflag: false 和一个 diagnosticsdiagnostics 数组，报告内容与 VSCode 面板中显示的相同。数组中的每一项对应一个栈帧，记录文件、行、列，以及编译器或引擎的消息；消息包含失败的语句，如果有符号状态，也会一并给出。

小结

  • cstar_mcpcstar_mcp 通过 MCP 向 AI 助手提供验证器的功能：它随工具链发布，位于 ~/.cstar/bin~/.cstar/bin，在客户端中以标准输入输出服务器的形式注册，使用绝对路径，不带参数，并为每个文件启动独立的证明器。
  • 六个工具：cstar_showlspcstar_showlsp（某一行的符号状态，或文件作用域处的验证报告）、search_theoremssearch_theorems 与 search_conversionssearch_conversions、cstar_helpcstar_help（指南及其主题），以及用于恢复的 cstar_killlspcstar_killlsp 与 cstar_interruptcstar_interrupt。
  • 工作流与本教程相同：先做设计，查询右花括号所在行，阅读失败前后的状态，搜索、编辑后再次查询。“通过验证”要求查询文件真正的最后一行，且返回的 verification_conditionsverification_conditions、axiomsaxioms 与 strategiesstrategies 都为空。