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 skills add afhverjuekki/claude-code-aristotle-plugin --skill aristotle-workflowgit clone --depth 1 https://github.com/afhverjuekki/claude-code-aristotle-pluginWrote 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/skills/afhverjuekki/claude-code-aristotle-plugin/aristotle-workflow)<a href="https://agentmods.dev/skills/afhverjuekki/claude-code-aristotle-plugin/aristotle-workflow"><img src="https://agentmods.dev/badge/skills/afhverjuekki/claude-code-aristotle-plugin/aristotle-workflow/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/skills/afhverjuekki/claude-code-aristotle-plugin/aristotle-workflow"><img src="https://agentmods.dev/badge/skills/afhverjuekki/claude-code-aristotle-plugin/aristotle-workflow.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.00091 | $0.02143 |
| Opus 5 | $0.00046 | $0.01071 |
| Sonnet 5 | $0.00018 | $0.00429 |
| Haiku 4.5 | $0.00009 | $0.00214 |
Grade A, and why
Aristotle Workflow 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 9d 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 — 285 lines — stays where its author put it; the contents beside it link to each section on GitHub.
Aristotle: Theorem Proving & Code Verification
Overview
Aristotle is an AI system from Harmonic with two major capabilities:
- Theorem Proving - Gold-medal IMO 2025 performance (5/6 problems), solved open Erdos problems
- Code Verification - 96.8% accuracy on VERINA benchmark, verifies algorithm correctness
Key insight: Aristotle works best with hints. For theorems, provide informal proofs. For code, provide clear pre/postconditions.
Code Verification (VERINA-Style)
Aristotle verifies algorithm implementations against formal specifications. It either proves correctness or finds counterexamples.
Verification Structure
-- 1. PRECONDITION: Input constraints
def algorithm_precond (input : Type) : Prop := ...
-- 2. ALGORITHM: Implementation to verify
def algorithm (input : Type) (h : algorithm_precond input) : OutputType := ...
-- 3. POSTCONDITION: Required output properties
def algorithm_postcond (input : Type) (result : OutputType)
(h : algorithm_precond input) : Prop := ...
-- 4. SPECIFICATION: Verification goal
theorem algorithm_spec_satisfied (input : Type)
(h : algorithm_precond input) :
algorithm_postcond input (algorithm input h) h := by
sorry
Verification Outcomes
- Proof found: Algorithm is correct
- Counterexample: Bug detected, e.g.,
use [4, 1, 2, 1, 4], 2; native_decide - False detected: Specification or implementation is wrong
Verified Algorithms (Examples)
Aristotle has verified (from VERINA benchmark):
- Selection sort correctness
- Run-length encoding
- Longest increasing subsequence
- 160+ algorithm implementations
See references/code-verification.md for detailed code verification patterns.
Theorem Proving (Erdos-Style Workflow)
Follow this pipeline for best results:
1. Research/Understand problem
2. Write proof strategy (natural language)
3. Generate rigorous informal proof
4. Verify proof logic
5. Aristotle: Formalize to Lean ← PRIMARY USE
6. Fix Lean warnings
7. Verify no sorryAx contamination
What ships with it
9 files beside SKILL.md in the same directory: the scripts, references and assets a skill reads on demand. Not counted in the per-session cost; read them before you install if any of them is executable.
- examples/mathlib-theorem.lean 2.9 KB
- examples/selection-sort-verification.lean 4.8 KB
- examples/standalone-theorem.lean 2.4 KB
- references/advanced-workflows.md 3.8 KB
- references/architecture.md 2.6 KB
- references/code-verification.md 5.9 KB
- references/troubleshooting.md 4.3 KB
- scripts/create-standalone.sh 2.9 KB runs code
- scripts/verify-proof.sh 2.8 KB runs code
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.
- 9d ago First seen · 285 lines · 91 tokens per session scan A 718f71740fca
Aristotle Workflow is a skill published in the GitHub repository afhverjuekki/claude-code-aristotle-plugin (10 stars, last pushed 8mo ago), licensed MIT. It adds 91 tokens to every session and 2,143 once invoked, about $0.0005 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 skills, from other repositories
cran-extrachecks
Prepare R packages for CRAN submission by checking for common ad-hoc requirements not caught by devtools::check(). Use when: (1) Preparing a package for first CRAN release, (2) Preparing a package update for CRAN resubmission, (3) Reviewing a package to ensure CRAN compliance, (4) Responding to CRAN reviewer feedback.…
mirai
Help users write correct R code for async, parallel, and distributed computing using mirai. Use when users need to run R code asynchronously or in parallel, write mirai code with correct dependency passing, set up parallel workers, convert from future or parallel, use miraimap, integrate with Shiny or promises, or…
paper-opportunity-radar
Run a cumulative daily or retrospective sweep of research papers on a chosen topic, audit their claims, methods, integrity signals, and independent support, then identify overlooked but feasible project or business opportunities in a detailed source-grounded report. Use when asked to monitor papers every day, mine…
using-cesiumjs-skills
Use when starting any conversation involving CesiumJS development - provides orientation on available domain skills and how they activate.
paper-verification
Use when the user wants to verify paper claims against code or data, audit numerical accuracy, check formula-code alignment, or validate citation accuracy. Triggers on phrases like "verify claims", "check numbers", "do the numbers match", "formula vs code", "audit the paper", or "cross-check results".
paper-writing
Use when the user wants to write, structure, or revise academic paper sections, improve notation consistency, or refine figures and tables. Triggers on phrases like "write the abstract", "structure the methods", "improve this section", "notation consistency", "figure refinement", or "paper structure".