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 agents/verified-zkevm/evm-asm/proof-patternsgit clone --depth 1 https://github.com/Verified-zkEVM/evm-asmWhat 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.00000 | $0.08722 |
| Opus 5 | $0.00000 | $0.04361 |
| Sonnet 5 | $0.00000 | $0.01744 |
| Haiku 4.5 | $0.00000 | $0.00872 |
Grade A, and why
proof-patterns 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 3d 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 — 647 lines — stays where its author put it; the contents beside it link to each section on GitHub.
EvmAsm — Proof Patterns (deep reference)
Moved out of AGENTS.md to keep the agent guide compact. Load this when a proof you are
writing hits one of these symptoms; do not read end-to-end:
- Postconditions explode under
xperm→ §Bundling Postconditions withletBindings. - Adapter signatures become unwieldy with deep let-chains → §Adapter Signatures with Deep Let-Chains.
linarithfails on let-bound terms oromegablows upmaxRecDepth→ §linarith vs omega for Let-Bound Terms / §Pure-Nat Sub-Lemmas.- End-to-end composition needs existential intermediates → §End-to-End Composition with Existential Intermediates.
xpermhits scaling limits / atom-count cliffs → §XPerm Scaling Limits and Sub-Assertion Bundling.- Double-addback (
_da) postcondition shape needed → §Double-Addback (_da) Postcondition Pattern. - Folded framed post fights
xperm/whnf, orextract_pure/drop_puremisbehave → §Folded Framed Posts. - Tempted to copy the
7 * (2 ^ 64 - 1) + 11step bound into a new loop spec → §The 7×(2^64−1)+11 Step-Bound Idiom.
Each section is self-contained — jump to the matching heading instead of reading top-to-bottom.
The 7×(2^64−1)+11 Step-Bound Idiom
A number of cpsTripleWithin proofs carry a step bound of the form
7 * (2 ^ 64 - 1) + 11 (or the shared tailSteps wrapper, used as
1 + tailSteps / tailSteps + 5). Measured population: 26–32 theorems
across 12 files (census at 89cdd641a, GH #11461).
What it means, and why it is sound. The factor derives from the machine
counter's width — the loop decrements a 64-bit register, so the proof bounds
the trip count by the full u64 range — not from the data. It is sound
because a cpsTripleWithin bound is an upper limit (∃ k ≤ nSteps), so any
sufficiently large bound closes.
Stop-propagation clause. A NEW proof must not copy this idiom without first
asking whether a concrete length bound is available for the input in scope.
Every existing site has its input (byte list / listLen / count) present as
hypotheses, so a data-driven bound of the form 7 * length + C is available in
principle. Open prerequisite (#11461): no existing site carries a concrete
sub-2^64 cap on its input length — only the memory-overflow guards — so there
is nothing to tighten against until someone decides where such a cap comes
from. Until that is settled: record the looseness, do not copy the idiom.
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.
- 3d ago First seen · 647 lines · 0 tokens per session scan A 417562c5c532
proof-patterns is an agent published in the GitHub repository Verified-zkEVM/evm-asm (54 stars, last pushed 3d ago), licensed MIT. It costs nothing until one of its globs matches a file; then it loads 8,722 tokens. 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 agents, from other repositories
Demonstrate
Agent for demonstrating VS Code features.
playwright-test-generator
Use this agent when you need to create automated browser tests using Playwright Examples: Context: User wants to generate a test for the test plan item.
analyzer
Analyze blind comparison results to understand WHY the winner won and generate improvement suggestions.
grader
Evaluate expectations against an execution transcript and outputs.
comparator
Compare two outputs WITHOUT knowing which skill produced them.
.NET-Notebook-Migration-Agent
Expert .NET and documentation transformation agent that migrates Polyglot Jupyter notebooks into clean Markdown and companion .NET sample code.