Coding agents (MCP)

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 server with the spec and verification tools.

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:

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

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.
Call lemma.search with the same key. When performance is comparable, prefer the patterns existing lemmas cover: verification is faster and UNKNOWN is rarer.
Write the kernel and its @tfe.implements annotation together.
Call verify.quick. On a counterexample, fix the kernel using the witness, holds_when and suspect, then call it again.
When it passes, call verify.full, then tune performance. Performance work must keep verify.full passing.
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:

AGENTS.md

# 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.

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.

Get started

Concepts

Guides

Model conformance

Case studies

Help

Tools

The loop

AGENTS.md

​Tools

​The loop

​AGENTS.md

Tools

The loop

AGENTS.md