Agent Plugins Marketplace
← All plugins

agent-formal-verify

v0.3.3

Model-check protocols with TLA+, prove invariants with Lean 4, and check bounded Rust functions with Kani.

CodexClaude Code2 Skills

By Michael DenyerLicense: GPL-3.0-only3 GitHub starsUpdated 2 weeks ago

Directory evidence

Runtimes
Codex and Claude Code
Parsed components
2 skill or MCP entries
Source updated
Oct 5, 2026
Manifest status
Canonical path parsed

The directory validates manifest shape and source location. It does not execute the plugin or provide a security endorsement. Review the indexing methodology →

Install agent-formal-verify for Codex and Claude Code

Installs for the current user
codex plugin marketplace add michael-denyer/agent-formal-verify
codex plugin marketplace upgrade agent-formal-verify
codex plugin add agent-formal-verify@agent-formal-verify

Paste and run these commands in a terminal with Codex. They add and refresh the agent-formal-verify catalog, then install this plugin.

Compatibility: the page URL and API slug “agent-formal-verify” remain stable.

  • Codex: agent-formal-verify@agent-plugin-marketplace → agent-formal-verify@agent-formal-verify

The installer fetches third-party code from the source repository shown on this page. This directory validates manifest structure and source location, but does not perform a security audit; review the manifest, components, and source before installing.

Get the source manually
git clone https://github.com/michael-denyer/agent-formal-verify

Clone the source repository, then follow its setup instructions to add the plugin to a compatible client. The repository root is the plugin root.

Plugin files

agent-formal-verify/
├── .codex-plugin/plugin.json
├── .claude-plugin/plugin.json
├── skills/formal-verify/SKILL.md
└── skills/setup/SKILL.md

Included Skills2

formal-verifyskills/formal-verify/SKILL.md

Model-check thread protocols with TLA+ and TLC, prove sequential invariants with Lean 4, and check bounded Rust functions with Kani. Map counter-examples to source locations, reproductions and fixes, and keep the models in CI. Use for /agent-formal-verify:formal-verify, formal verification, model checking, Lean proofs, Kani, bounded Rust verification, or concurrency bugs that runtime tests cannot reproduce.

setupskills/setup/SKILL.md

Prepare all shared tools for the agent-formal-verify plugin: Java, Python, TLC, elan, Lean, Rust and Kani. Use for initial installation, missing prerequisites, or /agent-formal-verify:setup.

Plugin manifests2

.codex-plugin/plugin.json
{
  "name": "agent-formal-verify",
  "version": "0.3.3",
  "description": "Model-check protocols with TLA+, prove invariants with Lean 4, and check bounded Rust functions with Kani.",
  "author": {
    "name": "Michael Denyer",
    "url": "https://github.com/michael-denyer"
  },
  "homepage": "https://github.com/michael-denyer/agent-formal-verify",
  "repository": "https://github.com/michael-denyer/agent-formal-verify",
  "license": "GPL-3.0-only",
  "keywords": [
    "agent-formal-verify",
    "tla-plus",
    "tlc",
    "lean",
    "kani",
    "rust",
    "model-checking",
    "proofs",
    "skills"
  ],
  "skills": "./skills/",
  "interface": {
    "displayName": "Agent formal verify",
    "shortDescription": "TLA+, Lean and Kani verification with explicit tool setup",
    "developerName": "Michael Denyer",
    "category": "Developer Tools",
    "capabilities": [
      "Read",
      "Write"
    ],
    "defaultPrompt": [
      "Use formal-verify to model-check this protocol."
    ]
  }
}
.claude-plugin/plugin.json
{
  "name": "agent-formal-verify",
  "version": "0.3.3",
  "description": "Model-check protocols with TLA+, prove invariants with Lean 4, and check bounded Rust functions with Kani.",
  "author": {
    "name": "Michael Denyer",
    "url": "https://github.com/michael-denyer"
  },
  "homepage": "https://github.com/michael-denyer/agent-formal-verify",
  "repository": "https://github.com/michael-denyer/agent-formal-verify",
  "license": "GPL-3.0-only",
  "keywords": [
    "agent-formal-verify",
    "tla-plus",
    "tlc",
    "lean",
    "kani",
    "rust",
    "model-checking",
    "proofs",
    "skills"
  ]
}

For maintainers

If you maintain this plugin, link to this source-backed listing from your README so users can review its manifest and indexed components.

[agent-formal-verify on Agent Plugins Marketplace](https://pluginsmp.com/plugins/agent-formal-verify)