audit: resurrect Kani proof suite + 6 audit-gap proofs (Phase F + F+) - #85

Merged

dcccrypto merged 15 commits into

audit/kani-resurrect

Apr 18, 2026

Commits on Apr 6, 2026

fix: rename duplicate charge_fee_to_insurance (1-arg) to sweep_fee_debt_to_insurance

dcccrypto
and
claude
committed

Commits on Apr 16, 2026

fix(hygiene): annotate keeper_crank best-effort let _ patterns + guard force-realize counter

dcccrypto
and
claude
committed

Commits on Apr 17, 2026

test(kani): repair stale proof harnesses for Phase F compatibility
dcccrypto
committed
feat(kani): Phase F — 5 audit-gap proofs (healthy-immune, fee-bounded,
dcccrypto
committed
test(kani): resurrect tests/kani.rs (202 proofs) from upstream-divergence rot
dcccrypto
committed
test(kani): fix fast_maintenance_margin to include MM floor + pos_margin
dcccrypto
committed
test(kani): unwind bumps + LQ4 cap fix + fee_split zeroed in test_params
dcccrypto
committed
test(kani): 5 more proof fixes — unwind bumps + stale-crank rewrite + lq fee cap
dcccrypto
committed
test(kani): proof_gap1 conditional no-mutation (overflow unreachable)
dcccrypto
committed
test(kani): MAX_VAULT_TVL deposit fix + 3 bitwise-NOT bugs + 2 missing fees
dcccrypto
committed
test(kani): Phase F+ — 3-account haircut cascade topology proof

dcccrypto
and
claude
committed
Merge remote-tracking branch 'origin/master' into audit/kani-resurrect
dcccrypto
committed
test(kani): adapt P8321 funding proofs to Phase 3B Result<i64> signature

dcccrypto
and
claude
committed

Commits on Apr 18, 2026