Formal verification

[colin-morpho]

Meta issue to track the verification progress and requirements.

Properties:

• reentrancy safety, see Reentrancy safety. #14 and Colin@verif/reentrancy safety #15;
• immutability property, see Immutability #16 and Colin@verif/immutability #25;
• revert checks, see [Certora] Verify expected reverts #26 and [Certora] Verif expected reverts #37 ;
• ranges, see comment, see [Certora] Verif math is safe #89 ;
• liveness, i.e. preLiquidate always repays, see Verify that pre-liquidations repay #35 and Verif pre-liquidations repay #38 ;
• liveness, i.e. preLiquidate can be called with repaid assets or shares, see Pre-liquidation with shares succeeds. #71 and [Certora] Verify pre-liquidate with shares #72;
• meta-property pre-liquidation doesn't degrade position.

[MathisGD]

#32 (comment)

[MathisGD]

I guess that it was closed automatically when you merged the PR, but wasn't intended.

[colin-morpho]

Indeed, thank you Mathis!

[MathisGD]

We could verify the bound of #43 (#43 (comment)). I let you add it to the todo

[QGarchery]

Two other properties to try to verify:

• there can be no division by zero in the ltv computation
• the position ltv improves (or stays the same) after a liquidation

[colin-morpho]

There's WIP on these two properties.