Security & Audits

Formal verification

The RiskEngine invariants and BorrowMarket accounting were verified in Certora Prover. The most important proven invariants:

• No debt creation without collateral: for every borrow tx, ΔD ≤ CF · ΔC.
• Solvency: Σ D_i ≤ Σ Σ c_i,j · L_j · P_j after every state transition.
• Dividend accumulator conservation: Σ userReward + unclaimed = Σ streamed (± 1 wei rounding).
• Boost cap: for all i, b_i ≤ 2.5。
• Lock monotonicity: T_end is non-decreasing for any given lock NFT.

Operational security

• Timelock — 48h for any parameter or upgrade action.
• Guardian multisig — 4-of-7, may pause markets but cannot move user funds.
• Oracle deviation freeze — automatic, no human intervention.
• Circuit breaker — if 24h bcUSD mint exceeds 20% of supply, mint is throttled.