The proofs

Most AMMs ask you to trust them.
We'd rather you check.

The core math is machine-checked in Lean 4 — zero sorry — and the Solidity is differential-tested bit-for-bit against a 60-digit oracle. Everything's in the repo. This page is built to be quoted: every claim below links to the exact file that backs it.

Open the repo → Read the litepaper

✓ Lean 4 · 0 sorry ✓ 2,699 differential assertions ✓ 60-digit mpmath oracle ✓ Core pool · forge-std only Not audited yet

#formal

Formally verified in Lean 4.

The two hardest theorems in the design — the exact split of a trade across a tick boundary (SPEC §2.7) and dimension reduction when a stable is quarantined (SPEC §2.8) — are machine-checked in Lean 4, with zero sorry and only standard axioms. Not "we tested a lot." Proved.

exact_splitunique_splitboundary_placementprice_consistency crossing_continuityslice_sphere_iffslice_planeslice_classification equal_price_on_spherelift_consistency

What this does NOT mean: formal verification proves the math is correct — not that every line of Solidity is bug-free. That's what the differential tests are for — and an audit, which we have not done yet.

→ analysis/orbitalproofs/ · AxiomCheck.lean prints the axioms behind each theorem

#differential

Differential-tested vs a 60-digit oracle.

A high-precision Python reference engine (mpmath, 60 digits) computes every quote, invariant, and lifecycle step. The Solidity is checked against it bit-for-bit across full trade/lifecycle trajectories — 2,699 passing assertions back the reference paths.

# the exact command that runs it

forge test --match-contract Differential --ffi

[PASS] Solidity ≡ oracle across all trajectories

# all disagreement is pure Solidity rounding — it *calibrated* the tolerances:

EPS_F_REL: 1e6 → 1e4 (≈1900× the measured max dust, 5.33)

What this does NOT mean: the oracle is a reference, not a second implementation of the whole contract. It pins the math; reviewing the surrounding Solidity is an audit's job — and we have not done one.

→ analysis/reference_cli.py · contracts/SPEC_CALIBRATION.md

#tests

The Foundry suite + invariant fuzzing.

50+ tests (forge test --ffi): engine anchors from the manual, FFI differential tests vs the oracle, lifecycle behavior, and a stateful invariant campaign that fuzzes real trade/lifecycle sequences and asserts the core invariants hold after every call:

I1 · torus residual F ≤ 0I3 · classification bandI4 · solvency I5 · xAgg ≥ u (real ≥ 0)I9 · claims conservation

fuzz: 1024 runs · invariant: 256 runs × depth 32 · a calibration campaign tightened tolerances from measured dust, not guesses.

What this does NOT mean: tests show the behavior we thought to check. The proofs cover the cases we can't enumerate; an audit — which we have not done yet — looks for the ones we didn't think of.

→ contracts/test/ · contracts/test/invariant/OrbitalInvariant.t.sol

#audit

Audit — not started.

No independent audit has been done, and no firm is engaged yet. This is the open gap in the stack, and mainnet is gated on closing it — the report will be published here in full the day it lands. What we can say today: we keep the attack surface deliberately small — Solidity 0.8.24, Foundry, and the core pool on forge-std only. The vault and router layer uses OpenZeppelin (1 external runtime dependency); there are no others. A bug bounty goes live at launch.

We have not engaged an audit firm yet. When a report is public, it will appear here. We say not audited — never "audited" — until a report is public. Security & risk →

For the people who actually read the code

Check it yourself.

Three commands. Don't take our word for any of it.

git clone <repo> && cd contracts && forge test --ffi

echo '{"op":"state","n":4,"ticks":[{"p":"0.95","A":"1000"}],"history":[]}' | python3 analysis/reference_cli.py

cd analysis/orbitalproofs && lake build && lake env lean AxiomCheck.lean

Note: forge fetches trace signatures over the network — run it with your sandbox off.

How we build

The process is the moat.

Anyone can ship an AMM. The thing that's hard to copy is the pipeline every formula goes through before it touches your money:

1 → derive the math from first principles (SPEC + derivations)
2 → prove it in Lean 4 (zero sorry, standard axioms)
3 → build a 60-digit mpmath reference oracle
4 → implement in Solidity (0.8.24, via-IR)
5 → differential-test Solidity ≡ oracle, bit-for-bit
6 → fuzz the invariants after every call (I1–I9)
7 → calibrate tolerances from measured dust, not guesses
8 → independent audit (not started — no firm engaged)

Read the litepaper → Play the simulator