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/afhverjuekki/claude-code-aristotle-plugin/verify-codegit clone --depth 1 https://github.com/afhverjuekki/claude-code-aristotle-pluginWhat 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.00018 | $0.01230 |
| Opus 5 | $0.00009 | $0.00615 |
| Sonnet 5 | $0.00004 | $0.00246 |
| Haiku 4.5 | $0.00002 | $0.00123 |
Grade A, and why
verify-code 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 — 155 lines — stays where its author put it; the contents beside it link to each section on GitHub.
Aristotle Code Verification
Load the aristotle-workflow skill for comprehensive guidance.
Overview
Aristotle achieved 96.8% accuracy on the VERINA benchmark, proving algorithm correctness and finding bugs in implementations. Use this command to:
- Verify algorithm correctness - Prove implementations meet specifications
- Find bugs - Discover counterexamples when code is incorrect
- Validate specifications - Check if pre/postconditions are correctly stated
VERINA-Style Verification Structure
Code verification in Lean 4 uses four components:
-- 1. PRECONDITION: Assumed to hold before execution
def myAlgorithm_precond (input : Type) : Prop :=
-- conditions on input
-- 2. ALGORITHM: The implementation to verify
def myAlgorithm (input : Type) (h_precond : myAlgorithm_precond input) : OutputType :=
-- implementation
-- 3. POSTCONDITION: Must hold after execution
def myAlgorithm_postcond (input : Type) (result : OutputType)
(h_precond : myAlgorithm_precond input) : Prop :=
-- conditions on result given input
-- 4. SPECIFICATION THEOREM: The verification goal
theorem myAlgorithm_spec_satisfied (input : Type)
(h_precond : myAlgorithm_precond input) :
myAlgorithm_postcond input (myAlgorithm input h_precond) h_precond := by
sorry
If Given a Lean File ($ARGUMENTS)
-
Read the file: @$1
-
Identify the verification structure:
- Preconditions (
_precond) - Algorithm implementation
- Postconditions (
_postcond) - Specification theorems (
_spec_satisfied)
- Preconditions (
-
Check for missing components and help complete them
-
Submit to Aristotle:
uvx --from aristotlelib aristotle prove-from-file "$1" \
--no-validate-lean-project --no-auto-add-imports
- Interpret results:
- Proof found: Algorithm is correct
- Counterexample found: Implementation has a bug OR specification is wrong
- False detected: Aristotle proves the negation with concrete values
If Given an Algorithm Description
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 · 155 lines · 18 tokens per session scan A 06be99f47808
verify-code is a command published in the GitHub repository afhverjuekki/claude-code-aristotle-plugin (10 stars, last pushed 7mo ago), licensed MIT. It adds 18 tokens to every session and 1,230 once invoked, about $0.0001 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-31.
Other commands, from other repositories
audit-lean-axioms
Report what a Lean 4 project rests on — inherited sorry, nativedecide, and where its axiom dependence comes from.
why-this-axiom
Explain why a Lean declaration depends on an axiom, and whether that dependence could be rerouted.
reflect
Review pending memory candidates and promote durable project learnings into .claude/memory.
git
Git operations with intelligent commit messages and workflow optimization.
checklist
Generate a custom checklist for the current feature based on user requirements.
clarify
Identify underspecified areas in the current feature spec by asking up to 5 highly targeted clarification questions and encoding answers back into the spec.