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