V1Verified
A healthy loan can never be liquidated.
Integer (uint256) model of SIestaVault; overflow reverts in Solidity 0.8.
healthy_not_liquidatable · Nightshift/Vault.lean ↗TRANSPARENCY
Everything you need to check us.
Every pre-open prediction is stamped on Solana, every safety rule is a machine-checked proof, and every contract is public. Nothing here depends on trusting SIesta.
Verified · Formal proofs
Safety rules, proven by math.
Every safety rule below is written as a Lean 4 theorem about SIesta's own code. Proofs are generated by Harmonic's Aristotle and re-checked by Lean's kernel; a rule shows as verified only once its proof passes.
Properties proven
24 / 24
Proof checker
Lean 4 kernel
Fingerprint
a97614aa79d5…
Vault 8 of 8 proven
V0Verified
The Vault's health check means exactly: debt is no more than collateral value times the liquidation LTV.
Integer model; floor division as in Solidity.
healthy_iff · Nightshift/Vault.lean ↗V2Verified
A price rise never makes a healthy loan unhealthy.
Integer model.
healthy_mono_price · Nightshift/Vault.lean ↗V3Verified
Adding collateral never makes a healthy loan unhealthy.
Integer model.
healthy_mono_collateral · Nightshift/Vault.lean ↗V4Verified
Repaying debt never makes a healthy loan unhealthy.
Integer model.
healthy_anti_debt · Nightshift/Vault.lean ↗V5Verified
The Vault always rounds in the protocol's favour: a loan it calls healthy is healthy in exact arithmetic too.
Integer model.
healthy_conservative · Nightshift/Vault.lean ↗V6Verified
Liquidation bonuses are capped at 15%.
LLTV at most 100%.
lif_bounds · Nightshift/Vault.lean ↗V7Verified
Anything you can borrow within the SIesta limit is healthy at that same price.
Integer model; same oracle price at borrow time.
borrowLimit_healthy · Nightshift/Vault.lean ↗Guardian 6 of 6 proven
G1Verified
The Guardian's sale amount is never negative.
Real-number model; slippage below 100%; position solvent after slippage.
sellAmount_nonneg · Nightshift/Guardian.lean ↗G2Verified
The Guardian never sells more collateral than you have.
Real-number model; slippage below 100%; position solvent after slippage.
sellAmount_le_collateral · Nightshift/Guardian.lean ↗G3Verified
When the Guardian acts, it restores your loan exactly to your target health.
Real-number model (the contract rounds the sale down, so on-chain it can land a hair below target); slippage below 100%; position solvent after slippage.
sellAmount_reaches_target · Nightshift/Guardian.lean ↗G3bVerified
The Guardian never sells more than it needs to.
Real-number model; slippage below 100%; position solvent after slippage.
sellAmount_minimal · Nightshift/Guardian.lean ↗G4Verified
If selling can't help, the Guardian won't sell. It alerts you instead.
Real-number model; enforced in the contract, the keeper and the paper Guardian.
no_sell_when_insolvent · Nightshift/Guardian.lean ↗G5Verified
The Guardian only acts on loans that can still be saved by selling.
Real-number model; LLTV below 1 − slippage (true for every SIesta market).
healthy_gate_solvent · Nightshift/Guardian.lean ↗Oracle 6 of 6 proven
O1Verified
The fair value always stays between the lowest and highest market signal.
Weights non-negative and summing to 1 (proven by O1a).
blend_within_signals · Nightshift/Oracle.lean ↗O1aVerified
The Oracle's signal weights are never negative and always add up to 100%.
Real-number model of the normalisation in computeQuote.
normalize_invariant · Nightshift/Oracle.lean ↗O1bVerified
Learning from past accuracy can never produce a negative weight.
Real-number model of learnWeights.
learned_invariant · Nightshift/Oracle.lean ↗O2Verified
With the signals' agreement unchanged, confidence never rises while the market stays closed.
Dispersion held fixed; confidence also depends on how much the signals agree, which can change.
confidence_antitone · Nightshift/Oracle.lean ↗O2bVerified
More disagreement between the signals never raises confidence.
Real-number model before rounding.
confidence_antitone_dispersion · Nightshift/Oracle.lean ↗O3Verified
Confidence always stays between 35 and 98.
Real-number model before rounding (rounding keeps the bounds).
confidence_bounds · Nightshift/Oracle.lean ↗Cloak 4 of 4 proven
C1Verified
Cloak proofs can't be faked through number overflow.
Circuit range checks of 64, 40 and 14 bits; BN254 field.
capacity_fits · Nightshift/Cloak.lean ↗C1bVerified
The debt side of the Cloak comparison also stays inside its safe range.
Debt range check of 64 bits; GreaterThan(120).
need_fits · Nightshift/Cloak.lean ↗C2Verified
Inside the circuit's range, field arithmetic equals ordinary arithmetic.
Values below the field modulus.
field_val_eq · Nightshift/Cloak.lean ↗C4Verified
A Cloak proof made from rounded numbers still proves the real loan is solvent.
Collateral rounded down and debt rounded up before proving (as the app now does).
circuit_sound_rounding · Nightshift/Cloak.lean ↗What this does and doesn't cover. These proofs cover the mathematical models of SIesta's logic, which are tested against the live code. They do not replace a smart contract security audit. The code-to-model mapping and every known gap are published in MAPPING.md.
Verified using Harmonic's Aristotle. Manifest generated 2026-10-12 · commit ea1169c · manifest.json
Ledger · Solana
Every prediction, on the record.
Before each opening bell, the Oracle's predictions are written to Solana, so the track record can't be edited afterwards.
Reading Solana_
Contracts
Public, verifiable code.
Contracts
The Vault, Guardian and Oracle contracts are built and tested (15 contract tests and 37 checks against the Lean model all pass) and go live on Solana shortly. Their addresses will be listed here.