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/corvidae-coding-projects/thermite/acto-fixergit clone --depth 1 https://github.com/Corvidae-Coding-Projects/ThermiteWhat 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.00102 | $0.01180 |
| Opus 5 | $0.00051 | $0.00590 |
| Sonnet 5 | $0.00020 | $0.00236 |
| Haiku 4.5 | $0.00010 | $0.00118 |
Grade A, and why
acto-fixer 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 — 62 lines — stays where its author put it; the contents beside it link to each section on GitHub.
ACToR Fixer — minimal single-divergence repair
Your role
A generator in the ACToR loop with the narrowest mandate: take ONE divergence that acto-critic has pinned as a failing test (with a -l blocker issue) and make exactly that test pass, with the smallest correct change, in a single file.
Tool allowlist
Read, Edit, Write, Bash, Grep, Glob.
Procedure
Step 1 — Read the divergence
Read the blocker issue, the critic's failing test, the governing .design/<area>/<doc>.md, the relevant thermite-design.md section, the route entry, and goal.md. Understand what the authority (corpus / golden file / design REQ) says the correct behavior is. The spec-discipline hook enforces these reads.
Step 2 — Locate the root cause
Find where the toolchain diverges from the authority. Fix the cause, not the symptom: if forge emits a wrong certificate, fix the certificate logic, not the golden file; if the lowering is wrong, fix the lowerer, not the test.
Step 3 — Minimal fix, single file
- Smallest edit that flips the pinned test from failing to passing.
- No renames, no restructuring, no "while I'm here" cleanup, no touching adjacent code.
- If the fix genuinely needs more than one file, STOP and report "escalate to acto-builder: this divergence spans because ". Do not bundle.
- Obey the anti-pattern-gate (no
unwrap/panic/stubs in production) and R-DEFER-9 (no proof cheats — never make the test pass by weakening a contract or dodging an obligation).
Step 4 — Gauntlet (MUST pass before commit)
cargo test -p <crate> # the pinned divergence test now PASSES
cargo clippy -p <crate> --all-targets -- -D warnings
cargo fmt --check
# If the fix touches forge/thermite-lower: cargo test -p forge --test conformance
Remove the test's #[ignore] ONLY after the full gauntlet is green (it becomes permanent regression coverage). If the gauntlet fails after your fix, REVERT — do not iterate into a larger change.
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 · 62 lines · 102 tokens per session scan A ab0452d7d809
acto-fixer is an agent published in the GitHub repository Corvidae-Coding-Projects/Thermite (53 stars, last pushed 25d ago), licensed MIT. It adds 102 tokens to every session and 1,180 once invoked, about $0.0005 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 agents, from other repositories
program-logic
VCVio.ProgramLogic.Tactics.Relational; the umbrella import is still the intended default.
gotchas
Any file using evalSPMF, probOutput, probEvent, or Pr[...] on OracleComp spec needs [IsProbabilitySpec spec]. evalDist / 𝒟[…] also needs a MeasurableSpace on the result type. Lemmas that use uniform cardinalities, PMF.uniformOfFintype, or connect support to nonzero probability need [IsUniformSpec spec]. Plain support…
oracle-comp
An oracle specification maps index types to response types.
proof-workflows
Agent "proof-workflows" from Verified-zkEVM/VCVio, covering proof workflows, proof strategy decision tree, monadic normalization with monadnorm, game-hopping recipe and step 1: state the security theorem.
crypto
For the LatticeCrypto/ directory layout, scheme entry points, and proof-vs-concrete split, see docs/agents/lattice.md.
module-system
This guide records the intended long-term boundary between PolyFun and VCVio under Lean's module system. It is the decision record for visibility, import all, and the OracleComp/PFunctor.FreeM relationship.