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/rupakm/leslie/lean4-ic3git 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/commands/rupakm/leslie/lean4-ic3)<a href="https://agentmods.dev/commands/rupakm/leslie/lean4-ic3"><img src="https://agentmods.dev/badge/commands/rupakm/leslie/lean4-ic3.svg" alt="Measured on agentmods" 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 | $0.00032 | $0.03945 |
| Opus 5 | $0.00016 | $0.01972 |
| Sonnet 5 | $0.00006 | $0.00789 |
| Haiku 4.5 | $0.00003 | $0.00394 |
Grade A, and why
lean4-ic3 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 — 315 lines — stays where its author put it; the contents beside it link to each section on GitHub.
Lean4 IC3
Property-directed reachability for Lean4 invariant proofs. Drives a CEGAR loop over a structure-based invariant: probe each action, extract counterexamples-to-induction (CTIs) from residual goals, dispatch a generalizer subagent to propose new conjuncts, insert them as non-breaking structure fields, and iterate until inductive.
Prerequisite: The invariant MUST be a structure, not a flat ∧. Adding fields
is the whole point — it must be non-breaking for existing field accessors.
Usage
/lean4-ic3 File.lean::InvName --spec=specName --safety=safetyLemma
/lean4-ic3 ... --max-iters=8
/lean4-ic3 ... --decide-cti=auto --check-n=3
/lean4-ic3 ... --generalizer=manual # default on first run
/lean4-ic3 ... --generalizer=agent # dispatch ic3-generalizer
Inputs
| Arg | Required | Default | Description |
|---|---|---|---|
| target | Yes | — | File.lean::StructureName |
| --spec | Yes | — | Spec value used with action_cases (e.g. tlMessages) |
| --safety | Yes | — | Safety lemma the invariant must imply |
| --init-lemma | No | init_preserves_inv |
Base-case lemma name |
| --step-lemma | No | step_preserves_inv |
Inductive-step lemma name |
| --max-iters | No | 8 | Max new conjuncts added before giving up |
| --generalizer | No | manual | manual (prompt user) or agent (ic3-generalizer) |
| --decide-cti | No | auto | auto / off / always — concretize CTI via decide at small n |
| --check-n | No | 3 | n for decide-based CTI concretization |
Refuse to start if the target invariant is not a structure declaration — flat
conjunctions make non-breaking insertion impossible. Tell the user to refactor
first. (See CLAUDE.md "Invariant Composition: Use Structures, Not Flat Conjunctions".)
Actions
Phase 0 — Baseline snapshot
lean_diagnostic_messages(file)→ record sorry count + diagnostic baseline.lean_file_outline(file)→ discover invariant structure fields and action names.- Verify
init-lemmaandstep-lemmaexist (may containsorry; that is fine). - Snapshot the invariant structure declaration verbatim. This is the rollback point.
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 · 315 lines · 32 tokens per session scan A 4cd3a1a7c75f
lean4-ic3 is a command published in the GitHub repository rupakm/leslie (14 stars, last pushed 1mo ago), licensed Apache-2.0. It adds 32 tokens to every session and 3,945 once invoked, about $0.0002 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 commands, from other repositories
learn
Interactive teaching and mathlib exploration.
formalize
Interactive formalization — drafting plus guided proving.
autoformalize
Autonomous end-to-end formalization from informal sources.
derive
Save a clean reference derivation of a target equation or theorem to derivations/. Draws from course materials (textbook, lecture notes) rather than testing the user.
afsim-learn
Command "afsim-learn" from qingzhoupro/afsim-skill, covering /afsim-learn — 文档解析融入 skill, 使用方式, 方式一：提供文件路径, 方式二：直接粘贴文档内容 and 方式三：指定分类.
openehr-explain
One-stop router that explains or looks up any openEHR thing — auto-detects an archetype, a template, an RM/AM/BASE type, an RM structural concept, an ADL idiom, an AQL query or keyword, or a terminology code (replaces /archetype-explain, /template-explain, /type-spec, /rm-structure, /adl-idiom, /terminology).