Borrowing it
Nothing to install: this file belongs to rupakm/leslie. 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/rupakm/leslie/main/.claude/agents/ic3-generalizer.mdgit clone --depth 1 https://github.com/rupakm/leslieWrote 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/agents/rupakm/leslie/ic3-generalizer)<a href="https://agentmods.dev/agents/rupakm/leslie/ic3-generalizer"><img src="https://agentmods.dev/badge/agents/rupakm/leslie/ic3-generalizer/github.svg" alt="Measured on agentmods" height="20"></a>Or the 80×15 button, for a site that already has a row of RSS and ATOM ones. Only the verdict fits; the numbers stay here.
<a href="https://agentmods.dev/agents/rupakm/leslie/ic3-generalizer"><img src="https://agentmods.dev/badge/agents/rupakm/leslie/ic3-generalizer.svg" alt="Reviewed on agentmods" width="80" 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.00058 | $0.02235 |
| Opus 5.5 | $0.00023 | $0.00894 |
| Sonnet 5.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 1mo 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.
- 1mo ago First seen · 180 lines · 58 tokens per session scan A 27b61a322391
ic3-generalizer is an agent published in the GitHub repository rupakm/leslie (15 stars, last pushed 2mo ago), licensed Apache-2.0. It adds 58 tokens to every session and 2,235 once invoked, about $0.0002 per session on Opus 5.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].
Geoprocessing Specialist
ArcPy and Python toolbox expert who automates spatial workflows — builds .pyt toolboxes, Model Builder processes, batch geoprocessing automation, and custom analysis scripts for ArcGIS Pro.
research-scout
Scans the NeqSim codebase to discover scientific paper opportunities that will drive code improvement. Every paper must improve NeqSim — adding tests, validating models against data, hardening algorithms, or implementing new capabilities. Produces ranked, actionable topics that feed into the planner agent.
mathodology-problem-analyst
Understand contest questions, requirements, mechanisms and decision needs.
astronomical-instrumentation-scientist
Reasons from system-level error budgets, the diffraction limit and Strehl ratio, detector figures of merit, and resolving power through Zemax/Code V tolerancing, ETC radiometry, AO modeling, and on-sky standard-star commissioning while treating flexure drift, IR persistence, ghosts, and quasi-static speckles as…
epidemiology-research-agent
Research agent for epidemiology and public health.