Description

This is a compilation of formal verification rules performed on the Stakehouse codebase using Certora Prover; both teams jointly reviewed adherence to the defined rules. The verification rules and test plan were mostly written by Blockswap with inputs from the Certora team in technical implementation and logical correctness assurance. It was developed as a supplement to the smart contract audits and unit tests to ensure Stakehouse's functional correctness requirements are met.

Formal verification proofs were designed to avoid false positive (vacuous) rules and to ensure that created specifications maximized the number of possible states the system can cover. The tool is very powerful with a vast array of execution paths to cover the bytecode of Stakehouse smart contracts. Although the tool is only as powerful as the written specifications, the tests were able to uncover results infeasible to traditional testing tools.