> ## Documentation Index
> Fetch the complete documentation index at: https://docs.theformalera.com/llms.txt
> Use this file to discover all available pages before exploring further.

# Coding agents (MCP)

> Let the agent that writes your kernels read the spec and verify while it generates.

Disposable inference systems are mostly written by agents, so the most frequent caller of the verifier should be the agent itself. `theformalera mcp` starts an [MCP](https://modelcontextprotocol.io) server with the spec and verification tools.

```bash theme={"system"}
pip install "theformalera[mcp,triton,engine]"
theformalera mcp                         # stdio (default)
theformalera mcp --transport streamable-http
```

Run it from the root of a repository that has a `theformalera.toml` and a lock. For example, to register it with Claude Code:

```bash theme={"system"}
claude mcp add theformalera -- theformalera mcp
```

## Tools

| Tool | Input | Output |
| - | - | - |
| `spec.get` | Spec Key | The node's Lean 4 definition, formula, constants, tensors, shape and value domains |
| `spec.nodes` | Model key | The compute-graph nodes and this repository's coverage |
| `verify.quick` | Annotated kernel source | A `quick`-level verdict with counterexamples (run JSON) |
| `verify.full` | Annotated kernel source | A job id for a `proof`-level run |
| `verify.job` | Job id | Status and result of `verify.full` |
| `explain` | Failure id | Counterexample, failing region and suspect line |
| `lemma.search` | Spec Key or subgoal text | Lemmas covering the node: the implementation patterns that verify fastest |

`verify.quick` and `verify.full` verify the source in a scratch copy of the project, against the project's locked specs, with the local engine.

## The loop

1. Call `spec.get` for the node you are implementing. Implement that definition, not the reference modeling file. The Lean definition is unambiguous: Qwen3.8's `(1 + w)` RMSNorm weight is spelled out.
2. Call `lemma.search` with the same key. When performance is comparable, prefer the patterns existing lemmas cover: verification is faster and UNKNOWN is rarer.
3. Write the kernel and its `@tfe.implements` annotation together.
4. Call `verify.quick`. On a counterexample, fix the kernel using the witness, `holds_when` and `suspect`, then call it again.
5. When it passes, call `verify.full`, then tune performance. Performance work must keep `verify.full` passing.
6. Open the PR. CI is the final gate.

## AGENTS.md

`theformalera init` writes an `AGENTS.md` with these rules, so any agent working in the repository follows them:

```markdown AGENTS.md theme={"system"}
# Kernel verification rules (theformalera)

Every GPU kernel in this repository is formally verified against a Lean 4 spec from Spec Hub.

1. **Read the spec before writing a kernel.** Call the MCP tool `spec.get` with the node's Spec Key
   (e.g. `Qwen/Qwen3.8-27B@1.0:layers[*].input_norm`) and implement exactly that definition — not the
   reference modeling file. Constants (hidden size, ε, head counts) come from the spec. Then call
   `lemma.search` with the same key: when performance is comparable, prefer the implementation
   patterns existing lemmas already cover — verification is faster and UNKNOWN rarer.
2. **Annotate every kernel.** Put `@tfe.implements(<spec key>, grid=..., bind=...)` on each
   `@triton.jit` kernel (or on its launcher), and `// @theformalera implements = ...` before each
   CUDA/CUTLASS kernel. A kernel under `require_annotation` without an annotation fails CI.
3. **`verify.quick` must pass before you commit.** If it reports a counterexample, use its witness,
   `holds_when` and `suspect` line to fix the kernel, then run it again. Never weaken an annotation's
   `domain` or add `assume` entries to make a check pass.
4. **Run `verify.full` once quick passes**, then tune performance. Performance work must keep
   `verify.full` passing.
5. Open the PR; `theformalera / verify` is a required check.
```

> [!WARNING]
>
> An agent can make a check pass by narrowing `domain` or adding `assume` entries. Reviewers should treat any change to those fields as a change to the contract. Both appear in the JSON report and in the release certificate.


This documentation is built and hosted on [Mintlify](https://mintlify.com), a developer documentation platform.