AI-Assisted Verification with cstar_mcp

The previous two sections showed how to automate two parts of a proof: strategies match and cancel spatial resources, and an SMT solver closes the remaining pure goals. Before writing the first proof block, we still need to choose a logical model for the data, define the predicate family, select loop invariants, and identify lemmas to fill gaps in the proof. So far in this tutorial, a person has made these choices by reading symbolic states in VSCode. cstar_mcpcstar_mcp lets an AI assistant follow the same workflow. 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 assistant’s MCP client using 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 the MCP counterpart of Show Symbolic StateShow Symbolic State, with the same source-location rules as the VSCode command: querying a line inside a function shows the state after that line, and querying a file-scope line returns the verification report accumulated up to that point. A file counts as verified only when a query at its actual last line returns empty verification_conditionsverification_conditions, axiomsaxioms and strategiesstrategies. The first query on a file is slow because it starts that file’s prover and builds its warm daemon. Later queries on the same file return quickly, and the daemon processes edits automatically. 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 incurs no startup cost. Querying a fourth file evicts the least recently used one, and the reply reports the eviction in a notenote.

The guide provided by cstar_helpcstar_help describes the same workflow we have followed manually in this tutorial:

1. first design the logical model of the data, the predicate family, function contracts, and the fold and unfold lemmas; then write the code and its proof blocks. For recursive functions, properties such as bounds on the size or height of the result can be stated in the postcondition, making them directly available after each recursive call;
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 a theorem or conversion that fills the gap;
5. edit the proof block and query again, with the file now warm;
6. finish with a query at the file’s last line, where all three lists must be empty.

Take the twicetwice function from Forward Proof in C* and save it as twice.ctwice.c in its own project; line 12 is int r = a + b;int r = a + b; and line 27 is the function’s closing brace. The following three calls show the assistant’s requests and the server’s replies (long values are trimmed; paths may be absolute or relative to the directory in which the server was started):

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

This is the same state shown in the VSCode panel at that line, with the unsimplified sum in the rr cell. Querying the last line returns the verification report. 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 theorem 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 contains flag: falseflag: false and a diagnosticsdiagnostics array with one entry per stack frame. Each entry records the file, line, column, and the compiler’s or engine’s message, including the failing statement and, when available, the symbolic state. This is the same report shown 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 follows this tutorial: design first, query the closing brace, read the state around a failure, search, edit, and query again. “Verified” means empty verification_conditionsverification_conditions, axiomsaxioms and strategiesstrategies at the file’s actual last line.