docs: update README

Author: QGarchery

certora/README.md

@@ -95,7 +95,7 @@ where `sumSupplyShares` only exists in the specification, and is defined to be a
 To ensure proper collateralization, a liquidation system is put in place, where unhealthy positions can be liquidated.
 A position is said to be healthy if the ratio of the borrowed value over collateral value is smaller than the liquidation loan-to-value (LLTV) of that market.
 This leaves a safety buffer before the position can be insolvent, where the aforementioned ratio is above 1.
-To ensure that liquidators have the time to interact with unhealthy positions, it is formally verified that this buffer is respected.
+To ensure that liquidators have the time to interact with unhealthy positions, it is formally verified that this buffer is respected and that it leaves room healthy liquidations to happen.
 Notably, it is verified that in the absence of accrued interest, which is the case when creating a new position or when interacting multiple times in the same block, a position cannot be made unhealthy.
 
 Let's define bad debt of a position as the amount borrowed when it is backed by no collateral.
@@ -249,11 +249,12 @@ The [`certora/specs`](specs) folder contains the following files:
   This includes checking that the accounting of the total amount and shares is correct, that markets are independent from each other, that only enabled IRMs and LLTVs can be used, and that users cannot have their position made worse by an unauthorized account.
 - [`ExactMath.spec`](specs/ExactMath.spec) checks precise properties when taking into account exact multiplication and division.
   Notably, this file specifies that using supply and withdraw in the same block cannot yield more funds than at the start.
+- [`ExchangeRate.spec`](specs/ExchangeRate.spec) checks that the exchange rate between shares and assets evolves predictably over time.
 - [`Health.spec`](specs/Health.spec) checks properties about the health of the positions.
   Notably, debt positions always have some collateral thanks to the bad debt realization mechanism.
 - [`LibSummary.spec`](specs/LibSummary.spec) checks the summarization of the library functions that are used in other specification files.
+- [`LiquidateBuffer.spec`](specs/LiquidateBuffer.spec) checks that there is a buffer for liquidatable positions, before they are insolvent, such that liquidation leads to healthier position and cannot lead to bad debt.
 - [`Liveness.spec`](specs/Liveness.spec) checks that main functions change the owner of funds and the amount of shares as expected, and that it's always possible to exit a position.
-- [`ExchangeRate.spec`](specs/ExchangeRate.spec) checks that the exchange rate between shares and assets evolves predictably over time.
 - [`Reentrancy.spec`](specs/Reentrancy.spec) checks that the contract is immune to a particular class of reentrancy issues.
 - [`Reverts.spec`](specs/Reverts.spec) checks the condition for reverts and that inputs are correctly validated.
 - [`StayHealthy.spec`](specs/Health.spec) checks that functions cannot render an account unhealthy.