Borrowing it
Nothing to install: this file belongs to yamafaktory/formal. Take a copy, put it at the same path in your own repository, and replace the rules that are about this project with yours.
curl -O https://raw.githubusercontent.com/yamafaktory/formal/main/.claude/commands/prove.mdgit clone --depth 1 https://github.com/yamafaktory/formalWrote this? Show the measurements
A badge with what this costs and how it scanned, read live from this page, so it follows the numbers instead of freezing them. Markdown for a README, HTML for a documentation site or a project page.
[](https://agentmods.dev/commands/yamafaktory/formal/prove)<a href="https://agentmods.dev/commands/yamafaktory/formal/prove"><img src="https://agentmods.dev/badge/commands/yamafaktory/formal/prove/github.svg" alt="Measured on agentmods" height="20"></a>Or the 80×15 button, for a site that already has a row of RSS and ATOM ones. Only the verdict fits; the numbers stay here.
<a href="https://agentmods.dev/commands/yamafaktory/formal/prove"><img src="https://agentmods.dev/badge/commands/yamafaktory/formal/prove.svg" alt="Reviewed on agentmods" width="80" height="20"></a>What it costs to keep this loaded
Counted locally with the o200k_base tokenizer, which is exact for GPT models; Claude uses its own tokenizer and its counts differ. Treat this as one consistent yardstick across the catalogue rather than a bill. Prices are per million input tokens.
| Model | Per session | Once invoked |
|---|---|---|
| Fable 5.1 | $0.00012 | $0.01324 |
| Opus 5.5 | $0.00005 | $0.00530 |
| Sonnet 5.5 | $0.00002 | $0.00265 |
| Haiku 4.5 | $0.00001 | $0.00132 |
Grade A, and why
prove scanned grade A with 0 findings against 26 rules in 11 categories — prompt injection, anti-refusal, data exfiltration, privilege escalation, supply chain, agent snooping, system-prompt leakage, SSRF and excessive agency — measured 2mo ago.
A static scan of the body, not an audit. Every finding is printed with the line that produced it so you can judge whether it matters here. A mod is markdown that instructs an agent; that is exactly why what it instructs is worth reading.
Nothing flagged
None of the 26 patterns this scan looks for appear in this file: no shell pipes, no recursive deletes, no credential paths, no hidden text, no instruction-override or anti-refusal phrasing, no agent-config snooping. That is not a guarantee, it is the absence of the things that are checkable.
How it starts
The opening of the file, as written. The whole thing — 104 lines — stays where its author put it; the contents beside it link to each section on GitHub.
Point formal at its own Rust and come back with proved properties. You are not here to change the Rust.
Target for this run: $ARGUMENTS — if that is empty, take the first entry under "Where to aim" that has no properties yet. One target per run. Stop when it is done rather than moving on; a long run costs more than two short ones and reviews worse.
Read README.md §"Driving formal from an agent" and CLAUDE.md first. The guide served
over HTTP is the authority on the workflow — this file only says what is already done,
what to aim at, and what not to break.
What already exists
formal.properties.json holds three properties, all against
rust/formal-core/src/proof_cache.rs, with their Lean in proofs/:
normalise_code/length_non_increasing, framed/shifting_a_boundary_changes_the_payload,
normalise_formal/word_operators_respect_boundaries. Two of the three were written after
formal found a real cache-key collision. Do not restate them.
Everything else in the workspace is unproved.
Running it
The binary is not on PATH, so the README's bare formal … will not work. From
rust/:
cargo run --bin formal -- status # expect: mathlib oleans built, sandbox bubblewrap
cargo run --bin formal -- serve --background # returns once /health answers; no-op if already up
cargo run --bin formal -- stop
It serves on http://127.0.0.1:1337.
The loop
GET /guide the workflow and the spec-file schema
GET /guide/extract how to find pure functions and properties
POST /session {"spec_file": "<absolute path to formal.properties.json>"}
GET /guide/formalize Lean 4 conventions for stating a property
GET /guide/tactics read before writing a proof, not after it fails
POST /session/{id}/check {"proofs": {"<id>": "<lean>"}}
spec_file must be absolute — the server's working directory is not yours.
/guide/{topic} takes exactly extract, formalize, tactics.
What this file has done since we first saw it
Hashed on every crawl. A supply-chain change to an agent config is a question of when, not whether, so the history is kept rather than the latest state alone.
- 2mo ago First seen · 104 lines · 12 tokens per session scan A e4202918915e
prove is a command published in the GitHub repository yamafaktory/formal (25 stars, last pushed 29d ago), licensed MIT. It adds 12 tokens to every session and 1,324 once invoked, about $0.0000 per session on Opus 5.5. A static security scan graded it A with 0 findings. No closer match exists in the catalogue, so it is treated as the original; first seen 2026-08-30.
Other commands, from other repositories
session
Complete guide to managing pair programming sessions.
expect
Diff-aware AI browser testing — reads the git diff, maps changes to affected pages via the route map, generates a targeted test plan, and executes it via agent-browser (Rust daemon + CDP, ARIA-tree-first) with pass/fail reporting. Use when testing UI changes, verifying PRs before merge, or running regression checks on…
generate-widget
Génération Widget Flutter avec Tests.
test-suite
Run comprehensive test suite with coverage analysis.
email-test-suite
../../services/email/email-test-suite.md.
AGENTS
Run the current binary in a temporary test repository with a real PTY. Use tmux-cli when available, capture terminal output, and inspect -vv logs when behavior depends on timing or shell state. Avoid treating a piped command as proof of interactive behavior.