Security & risk
Read this before you deposit.
LPing carries risk of loss. Providing liquidity is not risk-free. You can lose money.
Smart-contract risk exists. Code can have bugs. Formal verification and testing reduce risk — they do not eliminate it.
No third-party audit has been done yet. We have not engaged an audit firm. What we have instead is machine-checked proofs of the core math and differential testing against an independent 60-digit reference implementation — see the matrix below for exactly what that does and does not cover.
Do not deposit more than you can afford to lose. No yields are promised. There is no token and no airdrop.
What's verified — and what isn't.
Honesty is the product. Here's the real matrix.
| Layer | Status | How |
|---|---|---|
| Core math (exact split, dimension reduction) | ✓ Formally verified | Lean 4, zero sorry, standard axioms |
| Solidity numerics / rounding | ✓ Differential-tested | Bit-for-bit vs a 60-digit mpmath oracle · 2,699 assertions |
| Runtime invariants (F ≤ 0, band, solvency, claims) | ✓ Fuzzed | Stateful invariant campaign, asserted after every call (I1–I9) |
| Full contract (all paths, economic edge cases) | — Not audited | No audit firm engaged yet; mainnet is gated on this |
| Economic / oracle assumptions, keeper liveness, guardian trust | — Stated, not eliminated | Minimized and documented below — not removed |
Who can act on the pool.
The trust surface is deliberately small and auditable. Here's exactly who can do what, and why.
freeze() / poke()settle (realizing a quarantined asset) — sits behind an owner queue → timelock → execute flow. No instant, unilateral settlement. queueSettle → settleFull mechanism: SPEC §7 (lifecycle) and §9 (governance). Contracts are open and verified on-chain at launch.
Known limitations (v1).
Being first to list your own limits is a credibility flex. From SPEC §8.5:
- No trading fees in v1. The manual and the proofs are feeless; an input-side fee hook is stubbed but disabled. LPs earn no trading-fee yield in v1 (and we never promise yield).
- 18-decimal tokens only. Non-18-decimal tokens must be wrapped/scaled; they're rejected otherwise.
- No fee-on-transfer tokens. Rebasing / transfer-tax tokens are not supported in v1.
- Off-parity settlement is out of scope. Haircut/auction settlement of a badly-depegged asset is not in v1.
- Permissionless lift funding, flash accounting — out of scope for v1.
- The freeze-trigger oracle module ships as a swappable interface; treat its assumptions as stated, not eliminated.
Bug bounty & responsible disclosure
A bug bounty goes live at launch. If you find something, tell us privately first — we operate under safe-harbor for good-faith research. Please don't test on mainnet funds or publicly disclose before a fix.
security@spherra.xyz · PGP key on request
Audit status
Not audited. No firm is engaged yet. We will not deploy to mainnet without one; when a report exists it will be embedded here, and this page (plus the proofs page) will name the firm and link it. Until then, treat the verification we have done as exactly what it is — proofs of the math, not a review of the deployment.
Status: not started · firm: none engaged · report: none
Contracts & addresses
Verified source and mainnet addresses will be published here at launch. Until then, everything is in the public repo.
FreezeTrigger: — published at mainnet —
Chain / network: — announced at mainnet —