[Certora] Guard liquidateAtCapRestoresHealth against bad-debt vacuity - #1122

Open

claude[bot] wants to merge 21 commits into

mainfrom

claude/max-repaid-healthy-baddebt-guard

Commits on Aug 4, 2026

[Certora] Guard liquidateAtCapRestoresHealth against bad-debt vacuity
claude
committed
a43821d
[Certora] Prove liquidateAtCapRestoresHealth is revert-free
claude
committed
9be13e8
[Certora] Add liquidate's non-revert preconditions for revert-freedom
claude
committed
0255092
[Certora] Model mulDiv overflow deterministically for revert-freedom
claude
committed
4eefdb3
[Certora] Require msg.value == 0 for liquidate revert-freedom
claude
committed
cb871fb

Commits on Aug 31, 2026

Merge the base branch, de-duplicating the shared mulDiv-axiom refactor

claude
and
MathisGD
committed
d9c8093
[Certora] Keep the base branch's one-line rule comment

claude
and
MathisGD
committed
962c216
[Certora] Merge jhoenicke's axiom comments from #1083 base

claude
and
MathisGD
committed
82188ca
[Certora] Merge #1083 af632555 (cur -> old rename) into bad-debt guard

claude
and
MathisGD
committed
6473734

Commits on Sep 1, 2026