review

review is a command for coding agents from frenzymath/Archon. It costs 9 tokens per session (2,843 once invoked), scanned A, original, Apache-2.0.

A read-only reviewer for Lean4 proofs, where Lean4 is a programming language and proof checker for writing computer-verified mathematics. It examines selected files, lines, dependencies, or projects without changing them.

In plain words
What is it for?
Use it to review changed Lean files, a specific theorem or `sorry`, related dependencies, or an entire project. It can also produce structured JSON or use additional analysis options.
Why use it?
It finds quality, style, and optimization issues while leaving the code untouched. This gives you review feedback before you decide whether to edit the proofs.

Command

Part of the lean4 plugin — 1 skill, 11 commands, 4 agents, 3 hooks shipped together

Install

Getting it into your agent

One page per mod, every tool's command on it. A separate URL per tool would split the same page into five that compete with each other.

agentmods
npx agentmods add commands/frenzymath/archon/review
Clone the repo
git clone --depth 1 https://github.com/frenzymath/Archon

Or install lean4, the plugin that ships this one along with the rest of its 1 skill, 11 commands, 4 agents, 3 hooks.

Wrote 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.

agentmods badge for review

README.md
[![agentmods](https://agentmods.dev/badge/commands/frenzymath/archon/review.svg)](https://agentmods.dev/commands/frenzymath/archon/review)
Your own site
<a href="https://agentmods.dev/commands/frenzymath/archon/review"><img src="https://agentmods.dev/badge/commands/frenzymath/archon/review.svg" alt="Measured on agentmods" height="20"></a>
Per session 9 Only the description is in the session, so the agent can decide to use it. The body loads when it is invoked.
When invoked 2,843 The whole file, excluding the scripts and references it only reads on demand.
Security scan A 0 findings. Scan, not verified.
Origin original No closer match found in the catalogue.
Token cost

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.

ModelPer sessionOnce invoked
Fable 5 $0.00009 $0.02843
Opus 5 $0.00005 $0.01422
Sonnet 5 $0.00002 $0.00569
Haiku 4.5 $0.00001 $0.00284

Measured 5d ago against content hash 9beebea4c965, method: parsed. Prices are Anthropic first-party input rates as of 2026-08-30, from the pricing page.

Security

Grade A, and why

review 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 5d 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.

src/archon/.archon-src/skills/lean4/commands/review.md · 323 lines

How it starts

The opening of the file, as written. The whole thing — 323 lines — stays where its author put it; the contents beside it link to each section on GitHub.

Lean4 Review

Read-only review of Lean proofs for quality, style, and optimization opportunities.

Non-destructive: Files are restored after analysis.

Usage

/lean4:review                              # Review changed files (default)
/lean4:review File.lean                    # Review specific file
/lean4:review File.lean --line=89          # Review single sorry
/lean4:review File.lean --line=89 --scope=deps  # Review sorry + its dependencies
/lean4:review --scope=project              # Review entire project (prompts)

Inputs

Arg Required Description
target No File or directory to review
--scope No sorry, deps, file, changed, or project
--line No Line number for single-sorry scope
--codex No External review via Codex (interactive handoff)
--llm No Use llm CLI with model
--hook No Run custom analysis script
--json No Output structured JSON for external tools
--mode No batch (default) or stuck (triage)

Scope Behavior

Scope levels:

Scope Description
sorry Single sorry at --line (requires target file + --line)
deps Sorry + same-file helpers and directly referenced lemmas (requires target file + --line)
file All sorries in target file
changed Files modified since last commit (git diff)
project Entire project (requires confirmation)

Defaults:

  • No args → --scope=changed
  • Target file provided → --scope=file
  • Target + --line--scope=sorry
  • Triggered by prove/autoprove → matches current focus (sorry or file)

Note: Scope filtering is implemented by the reviewing agent, not the underlying scripts. The agent reads script output and filters results to match the requested scope.

Project-wide confirmation:

⚠️  This will review the entire project.
Proceed? (yes / no)

Output header always shows scope:

## Lean4 Review Report
**Scope:** Core.lean:89 (single sorry)

Read the full file on GitHub · 323 lines

Changes

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.

  1. 5d ago First seen · 323 lines · 9 tokens per session scan A 9beebea4c965

Subscribe to this mod's changes

review is a command published in the GitHub repository frenzymath/Archon (213 stars, last pushed 18d ago), licensed Apache-2.0. It adds 9 tokens to every session and 2,843 once invoked, about $0.0000 per session on Opus 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.