V1Verified
A healthy loan can never be liquidated.
Integer (uint256) model of NightshiftVault; 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 Algorand, every safety rule is a machine-checked proof, and every contract is public. Nothing here depends on trusting Nightshift.
Verified · Formal proofs
Safety rules, proven by math.
Every safety rule below is written as a Lean 4 theorem about Nightshift'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 Nightshift 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 Nightshift 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 Nightshift'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
Activity · On-chain
Proof it's running.
Every flow, counted from the chains themselves: loans, repayments, Guardian rules, Oracle updates, proofs and predictions. Each tile links to its latest transaction.
Reading Base and Algorand…
Ledger · Algorand
Every prediction, on the record.
Before each opening bell, the Oracle's predictions are written to Algorand, so the track record can't be edited afterwards.
Reading Algorand_
Contracts