The Certora Prover demonstrated that the implementation of the Solidity contracts is correct with respect to the formal rules written by the Certora team based on the inputs of the Liquity team.