AI-Assisted Verification with cstar_mcp

The previous two sections automated the two halves of a proof: strategies match and cancel spatial resources, and an SMT solver closes the pure goals that remain. What they do not decide is everything that comes before the first proof block — the logical model of the data, the predicate family, the loop invariants, the lemma that bridges a gap. In this tutorial that judgment has come from a person reading symbolic states in VSCode. cstar_mcpcstar_mcp hands the same loop to an AI assistant. It exposes the verifier over MCP (the Model Context Protocol), the interface through which AI assistants call external tools, so that an assistant can inspect the symbolic state at a line, search the theorem database, edit a proof block, and check again.

The server ships with the toolchain as ~/.cstar/bin/cstar_mcp~/.cstar/bin/cstar_mcp. Register it with your MCP client, whichever assistant you use, with these parameters:

• transport: standard input and output (a local process the client starts);
• command: the absolute path of the binary, /Users/you/.cstar/bin/cstar_mcp/Users/you/.cstar/bin/cstar_mcp, since the configuration is not read by a shell and ~~ is not expanded;
• arguments: none;
• environment: nothing required; CSTAR_MCP_MAX_STACKSCSTAR_MCP_MAX_STACKS raises the number of files kept warm (default three).

An assistant connected to the server sees six tools.

cstar_showlspcstar_showlsp is Show Symbolic StateShow Symbolic State under another name, with the same addressing rules as the VSCode command: a line inside a function shows the state after it, and a file-scope line carries the verification report gathered up to that point, so a file counts as verified only when a query at its real last line returns empty verification_conditionsverification_conditions, axiomsaxioms and strategiesstrategies. The first query on a file is slow, since it starts that file’s prover and builds its warm daemon; later queries on the same file return quickly, and the daemon picks up edits by itself. Up to three files stay warm at once by default (the CSTAR_MCP_MAX_STACKSCSTAR_MCP_MAX_STACKS environment variable raises the cap), each with its own prover, so switching between them costs nothing; a fourth evicts the least recently used one, and the reply says so in a notenote.

The guide that cstar_helpcstar_help serves spells out a workflow, and it is the one this tutorial has followed by hand:

1. design first — the logical model of the data, the predicate family, honest contracts with the recursion’s bounds in the postcondition, the fold and unfold lemmas — and only then the code and its proof blocks;
2. verify each function as it is finished, by querying its closing brace;
3. on a failure, query the executable lines before and after the proof block and read the state;
4. search the theorem and conversion databases for what bridges the gap;
5. edit the proof block and query again, now warm;
6. finish with a query at the file’s last line, where all three lists must be empty.

Take the twicetwice function of Forward Proof in C*, saved as twice.ctwice.c in a project of its own; line 12 is int r = a + b;int r = a + b; and line 27 the closing brace of the function. Three calls, as an assistant issues them and as the server replies (long values trimmed; paths are given absolute, or relative to the directory the server was started in):

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

It is the same state the VSCode panel showed at that line, with the unsimplified sum in the rr cell. The query at the last line returns the verification report instead, and all three lists are empty because the two proof blocks are in place:

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": [] },
    …
  }
}

A search returns names and statements, in the printer’s notation:

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"
  }
]

When a query fails, the reply carries flag: falseflag: false and a diagnosticsdiagnostics array with one entry per stack frame — file, line, column, and the compiler’s or engine’s message, with the failing statement and, when there is one, the symbolic state — the same report a person reads in the VSCode panel.

• cstar_mcpcstar_mcp exposes the verifier to AI assistants over MCP: it ships in ~/.cstar/bin~/.cstar/bin, is registered with the client as a stdio server by its absolute path with no arguments, and starts a prover of its own per file.
• Six tools: cstar_showlspcstar_showlsp (the symbolic state at a line, or the verification report at file scope), search_theoremssearch_theorems and search_conversionssearch_conversions, cstar_helpcstar_help (the guide and its topics), and cstar_killlspcstar_killlsp and cstar_interruptcstar_interrupt for recovery.
• The workflow is the one of this tutorial — design first, query the closing brace, read the state around a failure, search, edit, query again — and “verified” means empty verification_conditionsverification_conditions, axiomsaxioms and strategiesstrategies at the file’s real last line.