Introduction
Introduction
Machine-checked proofs of lottery odds, boost math, fee splits, and payout fractions. These check formulas — they do not replace Solidity audits or Foundry tests.
What this is
Aristotle (from Harmonic) helps produce formal proofs. Lean 4 is the language and checker that accepts or rejects those proofs.
In plain English: we write a math claim the way the contracts compute it, then ask Lean to verify that the claim is true for every input in the model — not just the cases we tested by hand.
What a proof means
- Model — the formula in Lean (floors, clamps, BPS), matched to onchain integer math.
- Claim — a property such as “raw boost is always between 1.0× and 2.5×.”
- Proof — a chain of lemmas Lean’s kernel accepts.
- Done — the project builds with no
sorry/admit. Those keywords are unfinished holes (“TODO / trust me”). Empty means every step is closed.
If Lean accepts the file, the claim holds under that model. It does not mean “the whole protocol is safe.”
Proofs vs audits vs tests
| What it checks | Best for | |
|---|---|---|
| June 2026 security review | Code review findings, architecture, severity | Bugs, trust boundaries, release readiness |
| Foundry tests | Specific inputs and regressions you pick | Implementation wiring, edge cases you thought of |
| Lean / Aristotle | All inputs in a stated math model | Envelope properties (“never exceeds 2.5×”) |
You want all three. Lean does not replace the Fable review or forge suites.
How 4626 uses it
Operators keep Lean artifacts under docs/audits/aristotle/<topic>/ in the repo. Public pages here summarize the readable claim, a worked example, the formula, and whether it is Proven or still queued.
Published claims
| Claim | Status | Read |
|---|---|---|
| Personal lottery boost is 1.0×–2.5× (Curve working balance + coverage blend) | Proven | Curve 2.5× boost |
| Base win chance ($1 → 0.0004%) | Proven | Base win chance |
| Boosted win chance never exceeds the hard cap | Proven | Post-boost pipeline |
| VRF roll matches the stated probability | Proven | VRF fairness |
| Fee split BPS sum to 100%; floor residuals go to burn or voters (no unpaid dust) | Proven | Fee-split |
| Jackpot pays 69% of reserve (not fees twice) | Proven | Jackpot payout |
How to read a claim page
- Plain claim — one sentence anyone can check against product docs.
- Worked example — numbers you can recalculate by hand.
- Formula — the onchain integer model.
- Proven / still open — whether Lean already accepted it (and which project / lemmas when proven).
What it does not mean
- Not whole-protocol formal verification.
- Not a substitute for Foundry or ops canaries (e.g. lottery boost sources may stay unset until enabled).
- Proofs are only as good as the model matching the Solidity. If code and model diverge, the proof is about the model.
Related product docs
The five Lean targets below are marked Proven with Aristotle project IDs and repo artifacts under docs/audits/aristotle/. Proven models cover the stated formulas only — not runtime config, operator keys, or off-model Solidity paths.
Was this page helpful?