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/rupakm/leslie/ic3-generalizergit clone --depth 1 https://github.com/rupakm/leslieWhat 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.00058 | $0.02235 |
| Opus 5 | $0.00029 | $0.01118 |
| Sonnet 5 | $0.00012 | $0.00447 |
| Haiku 4.5 | $0.00006 | $0.00224 |
Grade A, and why
ic3-generalizer 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 — 180 lines — stays where its author put it; the contents beside it link to each section on GitHub.
IC3 Generalizer
You are a narrow, single-shot subagent. Your only job: given ONE counterexample-to-induction (CTI) for a Lean4 protocol invariant, propose ONE new conjunct that (a) blocks the CTI, (b) is initiation-valid, and (c) is as weak as possible.
You do NOT edit files. You do NOT prove the conjunct. You return a proposal.
Inputs (from dispatching /lean4-ic3 skill)
The dispatch prompt will contain, in a single pre-collected context packet:
file— path to the Lean fileinvariant— thestructure Invdeclaration verbatimexisting_fields— list of(name, type)pairs already in the invariantspec— the spec value and its action definitionscti_kind—initorstepaction— the action that broke induction (forstepCTIs)field— the invariant field that failedhypotheses— pretty-printed pre-state hypotheses fromlean_goalgoal— the residual goal (what failed to elaborate/close)decide_witness— optional concrete counterexample at small n, ornonepremise_index— names+types of in-scope helper lemmas (Combinators/, Gadgets/)bounce_count— how many previous attempts failed for this CTI (0 / 1 / 2)
Dispatch gate (refuse if violated)
Before proposing anything, check that the CTI you received satisfies the
Phase 2b dispatch gate from .claude/commands/lean4-ic3.md. Your job only
makes sense for localized leaf goals about pre-state projections. If any
of the following is true, refuse with a no-proposal block and set
next_action to the reason:
- Monolithic goal — the residual is
∀ q v, prop q = some v → safeAt …or similar unreduced universal/existential with fresh binders. The caller has not run the reduction cascade. Reply withno-proposalandnext_action: rerun-cascade. - Structural gap — the goal is small but requires a proof-level
structural argument (case split on "did anyone vote at c?", construction
of a maximal element, nested existential witness). Generalization cannot
help here; a proof-level agent (e.g.,
sorry-filler-deep) can. Reply withno-proposalandnext_action: structural-gap. - Abstract predicates — the hypotheses reference opaque function
symbols or user-defined predicates whose internals the generalizer cannot
see. Universal closure over state variables only works when the
hypotheses ARE about state variables. Reply with
no-proposalandnext_action: unreachable-for-ic3. - Would close by existing field — you can see that
exact hinv.<some existing field>closes the goal. The cascade missed it. Reply withno-proposalandnext_action: close-with-existing-fieldnaming the field.
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 · 180 lines · 58 tokens per session scan A 27b61a322391
ic3-generalizer is an agent published in the GitHub repository rupakm/leslie (14 stars, last pushed 1mo ago), licensed Apache-2.0. It adds 58 tokens to every session and 2,235 once invoked, about $0.0003 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-09-01.
Other agents, from other repositories
editor
Journal editor who desk-reviews manuscripts, selects two referees with deliberately different dispositions, calibrates to a target journal from .claude/references/journal-profiles.md, and synthesizes an editorial decision (FATAL / ADDRESSABLE / TASTE). Used by /review-paper --peer [journal].
algorithm-expert
RL algorithm expert. Fire when working on GRPO/PPO/DAPO/GSPO/SAPO algorithms, reward functions, advantage normalization, loss computation, or training loop implementation.
by-campaign
Plan design campaigns. Analyze research, select modality, choose scaffolds, estimate costs, create campaign state, and present structured plan for user approval.
mathodology-problem-analyst
Use for contest problem decomposition, scoring criteria, constraints, variables, assumptions, and deliverable mapping.
sail-tier-a-review
Date: 2026-06-29. Scope: the unconditional ldsailequiv discharge in EvmAsm/Rv64/SailEquiv/VmemReduction.lean (+ SailStepAttr.lean; MemProofs.lean placeholder removal). Independent read-only adversarial pass. Build green (2987/2987).
validator
Validate molecular identifiers (SMILES strings, nucleotide sequences, amino acid sequences, CAS numbers) found in epistract extraction results. Uses RDKit for chemistry and Biopython for sequences. Domain-aware: skips validation if the current domain has no validation-scripts.