smart-contracts/backlog/tasks/task-15 - Security-Audit-and-Formal-Verification-of-Core-Contracts.md

id	title	status	assignee	created_date	labels	dependencies	priority
TASK-15	Security Audit and Formal Verification of Core Contracts	To Do		2026-04-03 21:42	security audit verification	TASK-2 TASK-3 TASK-4 TASK-5 TASK-7 TASK-8	high

Description

Comprehensive security review before mainnet deployment.

Scope:

• RiskTrancheManager.sol — waterfall correctness, reentrancy, precision loss
• ConvictionVoting.sol — overflow in conviction math, governance manipulation
• MycoBondingCurve.sol (enhanced) — invariant preservation, sandwich resistance
• MycoFactory.sol — proxy initialization, storage collision
• HubRegistry.sol + SpokeVault.sol — CCIP message validation, replay protection
• FlowDampener.sol — decay math correctness

Approach:

1. Internal review: Slither + Mythril static analysis
2. Fuzz testing: Echidna/Medusa property-based testing (invariants from cadCAD model)
3. Formal verification: Certora or Halmos for critical math (waterfall, conviction trigger)
4. External audit: Trail of Bits, OpenZeppelin, or Spearbit ($50-150K)
5. Bug bounty: Immunefi program post-launch

Critical invariants to verify:

• total_collateral >= sum(tranche_backing) at all times
• Senior CR >= target OR liquidation triggered
• Conviction monotonically increases with constant stake
• Cross-chain messages cannot mint unbacked tokens
• Factory clones initialize exactly once

Acceptance Criteria

• #1 Slither reports zero high/medium findings
• #2 Echidna property tests pass with 1M+ runs
• #3 Formal verification proves waterfall correctness
• #4 External audit completed with all findings addressed
• #5 Bug bounty program live on Immunefi