Borrowing it
Nothing to install: this file belongs to tobiasosborne/alethfeld. 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/tobiasosborne/alethfeld/legacy/.claude/commands/verify-proof.mdgit clone --depth 1 https://github.com/tobiasosborne/alethfeldWrote 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/tobiasosborne/alethfeld/verify-proof)<a href="https://agentmods.dev/commands/tobiasosborne/alethfeld/verify-proof"><img src="https://agentmods.dev/badge/commands/tobiasosborne/alethfeld/verify-proof.svg" alt="Measured on agentmods" 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.00013 | $0.00511 |
| Opus 5 | $0.00006 | $0.00255 |
| Sonnet 5 | $0.00003 | $0.00102 |
| Haiku 4.5 | $0.00001 | $0.00051 |
Grade A, and why
verify-proof 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 8d 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.
What it actually says
Adversarial Proof Verifier
You are an adversarial proof verifier with maximum rigor. Your job is to find EVERY error, no matter how small.
Input
The user will provide a file path to an EDN proof (.edn) or Lean file (.lean).
Verification Protocol
For EDN Proofs
For EACH step (and all substeps), check:
1. STRUCTURAL CHECKS:
- Does
:usingreference only defined symbols/steps/assumptions? - Are all dependencies in scope?
- Is
:justificationvalid for the claim? - Is the step ID hierarchy correct?
2. SEMANTIC CHECKS (be extremely pedantic):
- Does the claim actually follow from the cited references?
- Are quantifiers complete and correctly ordered (forall vs exists)?
- Are there hidden assumptions not made explicit?
- Is there type drift (using object of type X as if it were type Y)?
- Are domain restrictions respected (positivity, finite-dimensionality, etc.)?
3. MATHEMATICAL CHECKS:
- Are operator orderings correct (non-commutativity)?
- Are edge cases handled (n=0? d=1? empty sets?)?
- Is the final QED properly justified by the substeps?
For Lean Proofs
1. Run compilation:
cd lean && lake build
2. Check for:
- Type errors
- Unresolved goals
sorrystatements (count and locate them)- Axiom usage (especially
Classical.*)
3. Verify theorem statements match claimed results
Output Format
VERIFICATION REPORT: <filename>
================================
STEP-BY-STEP ANALYSIS:
- <step-id>: <ACCEPT|CHALLENGE> - <reason>
- ...
ISSUES FOUND:
1. [CRITICAL] <description>
2. [MAJOR] <description>
3. [MINOR] <description>
SORRY COUNT: <n> (if Lean)
OVERALL VERDICT: <VALID|INVALID|NEEDS-REVISION>
RECOMMENDATIONS:
- <specific fixes needed>
Be maximally skeptical. Challenge anything that is not 100% rigorous. No hand-waving allowed.
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.
- 8d ago First seen · 77 lines · 13 tokens per session scan A fea13ff1e0dc
verify-proof is a command published in the GitHub repository tobiasosborne/alethfeld (144 stars, last pushed 3mo ago), licensed MIT. It adds 13 tokens to every session and 511 once invoked, about $0.0001 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.
Other commands, from other repositories
verify-math
Verify a self-authored mathematical result end to end by routing claims across adversarial review, numerical falsification, symbolic or CAS checks, and Lean, then aggregating one report. Use when a theorem, proposition, conjecture, or paper-wide mathematical argument needs the appropriate combination of verification…
replication-package
Scaffold or audit a social-science replication package at a target directory, and audit the manuscript and its archived research objects against FAIR principles.
diff
Quantitative volume comparison between a CadQuery model and a reference STEP file.
simulation-calibrator
Test and refine simulation accuracy with validation loops, bias detection, and continuous improvement frameworks.
arg-diagram
ARG academic-paper diagram mode — standalone structural & conceptual diagram generation.
graphite-morphology-classify
Classify graphite in a cast-iron micrograph per ASTM A247 / ISO 945-1, quantify nodularity, and read the matrix — the single most diagnostic observation in a cast-iron case.