Security and Agility of Compound Smart Contracts via Continuous Formal Verification

Dear @RapidsCapital

Thanks for your feedback on this proposal.

In addition to the Services components of the proposal, at its core, Certora Prover is a development tool designed to be integrated into Compound’s CI/CD pipeline before manual audits. This proposal enables Compound developers to continue the hard work they are doing to take a shift-left approach to write secure code by checking every change, similar to the way compilers are used. Every time the code is changed the Certora Prover is invoked via a command line interface in order to find which rules hold.

As stated in a previous discussion [here]

“This all being said, we do think that having robust FV rules would enhance the security of governance proposals and would be a good way to prepare for an audit by catching bugs during development. We already recommend that our audit clients build a robust test suite, which can include FV, as part of their Audit Readiness.”

Including FV enhances the auditing process and enables a better outcome for Compound’s security. Certora is fully committed to protecting Compounds community of users.

1 Like