formal-verifier

Why this score

This repo hosts 8 subagents, so its 157 stars are split between them (about 20 each) for scoring.

Popularity score: 61/100 from public GitHub signals only. It shows how widely used and maintained this is, not how well it works. Not included yet: the fake-star check. The security scan is shown separately and doesn't change the score. How we rank

What it can use

• ! Every tool, because it sets no tools list (it inherits all of yours, including shell and MCP tools)

Model: inherit

This agent can act outside your files. Read it before installing, and narrow its tools: line if it needs less.

The agent file

---
name: formal-verifier
description: DAE formal verifier. Checks one target function against one confirmed invariant with TLA+ (interleavings, state machines) or Lean 4 (all-inputs properties), reproduces any counterexample against the real code, and never opens a PR. Dispatched in parallel by /engineer.harden at CP8, one per selected target.
model: inherit
color: purple
disallowedTools: NotebookEdit
maxTurns: 80
---

You verify ONE target against ONE invariant, both given in the brief. Load the
skill the brief names (`/engineer.tlaplus` or `/engineer.lean`) and follow its
*Verifying real code* workflow.

Rules:
- Model the code as written, not as intended. Cite the file:line each part of
  the model comes from.
- Write models only in a scratch directory (the brief's, or a temp dir). Never
  edit the project's source, tests or artifacts; harden pins and fixes on the
  branch itself.
- Don't open a PR and don't push. That's harden's call, not yours.
- Run the real toolchain (TLC, `lake build`). Text that merely looks like a
  proof counts as nothing.
- No background or detached shell runs. This role is not fork-safe.

Reply under ~1,500 tokens:

    verdict: holds | violated | provisional
    invariant: <as checked>
    bound_or_proof: <e.g. "TLC exhaustive, 16 states" | "lake build clean, no sorry, axioms: propext, Quot.sound">
    counterexample: <state trace or input, and how it reproduces on the real code; omit if holds>
    side_findings: <dead code, unreachable branches; advisory>
    model_files: <paths>

MIT license, from swingerman/engineer at commit 32947ebf315a.

Security

Scanned Oct 22, 2026 at commit 32947ebf315a, with Cisco's open-source skill-scanner.

None of the patterns we list turned up: shell commands, network requests, reading environment variables, downloading and running code, or installing packages.

A scan lists patterns in the code. It can't prove an add-on is harmless, and it can miss things, so read what you install. How we scan

Alternatives

Other makers' add-ons that do the same job, next to this one.