A skill for Claude Code, Codex, Pi and OpenCode that implements the targeted formal-verification method recently promoted by Boris Cherny. The agent models selected parts of your code, checks their properties, maps counter-examples to source lines, and helps reproduce and fix reachable bugs.
It uses TLA+ and TLC for thread interleavings, shutdown and resource ownership, and Lean 4 for arithmetic, bounds and sequential state transitions. A protocol that depends on arithmetic can use both. For Rust functions with bounded inputs and loops, Kani checks the production code for overflow, invalid memory access, panics and broken invariants.
Run in Claude Code:
/plugin marketplace add michael-denyer/agent-formal-verify
/plugin install agent-formal-verify@agent-formal-verify
Run in your terminal:
codex plugin marketplace add michael-denyer/agent-formal-verify
codex plugin add agent-formal-verify@agent-formal-verifyRun in your terminal:
pi install npm:agent-formal-verifyTo install from Git instead, use pi install git:github.com/michael-denyer/agent-formal-verify.
OpenCode 2.2 or later. Run in your terminal:
opencode plugin add agent-formal-verifyTo install from Git instead, use opencode plugin add 'git+https://github.com/michael-denyer/agent-formal-verify.git'.
Run setup once to prepare the shared Java, Python, TLC, elan, Lean, Rust and Kani tools. In Claude Code, use /agent-formal-verify:setup. In Codex, request the plugin's setup skill. In Pi, use /skill:setup. In OpenCode, request the setup skill. It reuses installed prerequisites and needs no target repository.
For local checkouts and skills-only installs, see shared installation.
Use formal-verify to check this queue's shutdown protocol and window arithmetic.
In Claude Code, use /agent-formal-verify:formal-verify. In Codex, type $formal-verify or request the plugin's formal-verify skill. In Pi, use /skill:formal-verify. In OpenCode, request the formal-verify skill.
The agent selects risky code, builds TLA+ or Lean models or adds Kani harnesses that call the Rust code, and checks their properties. Reachable counter-examples guide reproductions and fixes to both the code and model. Mutation checks test whether the properties detect mistakes. On request, a second agent reviews each model's properties against the code and proposes mistakes for those checks. CI reruns the models as the code changes.
A passing check establishes its stated properties under its assumptions and bounds. Reports must identify omitted constraints and unfinished proofs. See scope and evidence.
- Skills and slash commands
- Shared installation
- Runtime setup and tool pins
- Plugin updates
- Verification workflow
- Release history
- Agent instructions
The plugin configures no MCP servers or hooks, requires no credentials and has no telemetry. Its OpenCode entry point, opencode.mjs, only reads the bundled skill files and registers them; it runs no commands and makes no network requests. The agent sends selected source excerpts, models and results to its model provider. Helpers run locally and download nothing. Setup verifies a TLC JAR you obtain from the pinned TLA+ release, and Lean preparation installs the pinned toolchain through elan. Install the pinned Kani through Cargo and run its setup command as described in tool setup. The plugin's Kani helpers install nothing.
Bug reports, documentation fixes and runtime improvements are welcome. See CONTRIBUTING.md for development checks and pull requests.
Copyright (c) 2026 Michael Denyer. Licensed under the GNU General Public License, version 3, SPDX identifier GPL-3.0-only.