Plugin

formal

The prover side of research-kit: the harness of a prover session for a project that pairs its documents with a machine-checked library. It is built for Lean 4, the only prover it has run with: the manifest generator is a Lean program, and the agent’s tools are Lean’s language server. The bar it assumes is no sorry, admit or native_decide behind a landed declaration; formal.toml’s banned is another list, the phrases a handoff prompt may not carry. Another prover would need its own generator writing the same six row kinds, and none is written. It needs the research plugin; nothing in research needs it.

In Claude Code 2.1.275 or later it installs in one step, after the research plugin; Install covers every other agent:

/plugin install formal --marketplace lividgreen/research-kit

Three skills, an agent and a generator; the sections below take them one by one, with the commands of the formal script.

A prover handoff that is checked before it is sent

When work goes to a prover session, the agent composes the prompt statement-first from the document’s own text, with the declarations quoted, a refute-first line, the bundle’s shape and the witnesses commissioned, and checks it before dispatch. The prover session runs as a subagent, or the prompt is emitted for your own session.

The handoff skill and the prover agent

The handoff skill, /formal:handoff in Claude Code; formal handoffcheck DRAFT checks a drafted prompt’s decidable invariants before it is dispatched or emitted. The prover agent, formal:prover, is the prover session as a subagent: it reads the workspace’s standing instructions first, never commits, and ends with the report the landing verifies. A template of those instructions is workspace-instructions.md, which the setup fills in for the project.

A landing that reads the tree, not the report

Before any document changes, what the prover session reports is checked against the built library: the declaration manifest’s diff, a cold read-back of every landed statement, the binders and guards. The document’s rows are written from the landed proof, the summary sites swept, the records closed, and the commit names its paths.

The land skill

The land skill, /formal:land in Claude Code. formal handback prints the manifest diff, the instantiations, the witnesses owed, the guard delta, the document sites to re-read and the commission against the manifest; formal readback NAME… builds the docstring-stripped packet a cold reader writes each statement out from; formal check confirms the manifests parse and the bindings resolve. DeclManifest.lean, beside the script, generates a Lean package’s declaration manifest after a genuine build, writing the six row kinds formal and flow read.

The prover-side setup

/formal:formal-init reads the Lean workspaces under the root with their roots and toolchains, proposes what is missing, writes formal.toml, places the manifest generator, writes the prover session’s standing instructions from the template, and binds the flow’s declaration evidence and the formal-check hook.

The formal-init skill

The formal-init skill, /formal:formal-init in Claude Code; formal probe reports the workspaces, the tools and what the setup is missing, and writes nothing.

The script and the bindings

The plugin has one CLI, formal, and its script lives in the land skill (skills/land/scripts/formal.py, beside the generator), since landing is where every check of a report runs; the handoff skill calls the same script for handoffcheck and requires land. formal init writes formal.toml at the project root: the workspace and its instructions file, the manifests and how they are regenerated, the library roots with their package directories, the documents whose cited names are read at a landing, the handoff’s bans. The prover’s language server is registered by the project itself (its own .mcp.json), since the workspace path is the project’s; the agent uses whatever prover tools are registered. Claude Code’s copy of the agent, claude-agents/prover.md, pins model: sonnet: a prover session follows a checked handoff well on it and costs less than a larger model, which was the finding of the project research-kit was extracted from; the portable copy under agents/ inherits the session’s model, and a project that wants another model edits that line. GitHub Copilot, OpenHands and Antigravity read the agent from a directory of their own in the plugin, each holding the same text; Antigravity’s also lists the tools the prover needs, since Antigravity gives an agent only the tools it names. Which statement is proved next, how ties are ordered and what a wall is are the research plugin’s method skill, under “With a prover”. The rules these skills are written around come from that project, each contestable; the incidents behind them stay in its log, which is not public.