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/commands/lean4-ic3.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/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/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/commands/rupakm/leslie/lean4-ic3"><img src="https://agentmods.dev/badge/commands/rupakm/leslie/lean4-ic3.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.00032 | $0.03945 |
| Opus 5.5 | $0.00013 | $0.01578 |
| Sonnet 5.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 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 — 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.
- 1mo ago First seen · 315 lines · 32 tokens per session scan A 4cd3a1a7c75f
lean4-ic3 is a command published in the GitHub repository rupakm/leslie (15 stars, last pushed 2mo ago), licensed Apache-2.0. It adds 32 tokens to every session and 3,945 once invoked, about $0.0001 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 commands, from other repositories
client-education
Produce patient education handouts on specific dietary topics, conditions, or lifestyle modifications.
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.
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).
gpd:explain
Explain a physics concept rigorously in the context of the active project or a standalone question with an explicit topic.
thesis
Plan, structure, or strengthen a PhD/research thesis or dissertation in AEC.
talk
Turn a paper (or several) into an academic talk — outline, slides, speaker notes, backups, rehearsal plan.