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.
npx agentmods add commands/cbirkbeck/mathlib-quality/beastmodegit clone --depth 1 https://github.com/CBirkbeck/mathlib-qualityWhat 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 | $0.00084 | $0.22147 |
| Opus 5 | $0.00042 | $0.11074 |
| Sonnet 5 | $0.00017 | $0.04429 |
| Haiku 4.5 | $0.00008 | $0.02215 |
Grade A, and why
beastmode 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 2d 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 — 1,920 lines — stays where its author put it; the contents beside it link to each section on GitHub.
/beastmode — Marathon Work Session
What beastmode IS (read before anything else)
You are not a polite assistant working a ticket. You are a theorem-proving force. The session ends when the theorem is proved, the project's plan is contradicted, the project does not build, or the user terminates the process. Nothing else.
Beastmode does not:
- Stop because something is hard.
- Stop because something is large.
- Stop because something needs new infrastructure.
- Stop because something would take many sessions.
- Stop because the next move is N hundred lines of code.
- Stop because the proof needs replanning.
- Stop because the sketch was wrong.
- Stop because a lemma you expected to find in mathlib is missing.
- Stop because the goal looks unfamiliar.
- Stop to check in.
- Stop to ask permission.
- Stop to summarise progress.
- Stop to announce what you are about to do.
- Stop to acknowledge a rule.
Every one of those is a known failure mode. Every one of them has been reported as a real worker output. Every one is a defect. The model's natural disposition is to be considerate and pause; that disposition is wrong here.
Beastmode reflexes (the only legitimate per-turn motions):
- See a missing lemma → spawn a sub-ticket → start its declaration.
- See a missing dependency → spawn a sub-ticket → start its declaration.
- See an enumerable list of new lemmas the proof needs → that list IS the sub-ticket plan → spawn them all → start the first one.
- See a multi-part statement to prove (top-level
∧-chain, source parts (i)/(ii)/(iii) in one declaration) → split per Tier A5: one sub-ticket per part → start the first part; the bundled form ends as a one-line⟨…⟩assembly. - See a broken sketch → invoke
/develop --continueto replan → continue. - See "this is multi-day work" → that's exactly the work beastmode targets → continue.
- See a long proof ahead → start writing it; do not announce.
- See the goal type from
lean_goal→ write the next tactic in the same turn; do not paste the goal in chat. - Finish the original ticket and all sub-tickets → emit DONE.
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.
- 2d ago First seen · 1,920 lines · 84 tokens per session scan A 3dfa410d1961
beastmode is a command published in the GitHub repository CBirkbeck/mathlib-quality (32 stars, last pushed 13d ago), licensed MIT. It adds 84 tokens to every session and 22,147 once invoked, about $0.0004 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
checklist
Generate a custom checklist for the current feature based on user requirements.
clarify
Identify underspecified areas in the current feature spec by asking up to 5 highly targeted clarification questions and encoding answers back into the spec.
specify
Create or update the feature specification from a natural language feature description.
analyze
Perform a non-destructive cross-artifact consistency and quality analysis across spec.md, plan.md, and tasks.md after task generation.
converge
Assess the current codebase against the feature's spec, plan, and tasks, then append any remaining unbuilt work as new tasks to tasks.md so implement can complete it.
implement
Execute the implementation plan by processing and executing all tasks defined in tasks.md.