Certora Formal Verification Proposal

Thanks Shelly for renewing the discussion around continuous formal verification. I personally would like to see something like this adopted by the protocol as soon as possible, as formal verification with Certora has indeed been an important part of the quality assurance process we use for smart contract development at Compound Labs. I would very much like to see the community adopt a similar practice around all potential modifications to the protocol. I think the exercise of trying to articulate invariants about code being added or changed in itself helps increase the security of the protocol significantly, let alone the actual corner and counter cases discovered by running specific rules.

Certora is offering to help write rules, to teach the community how to write rules, and to run the rules on their servers. They are also offering to make their source code available to the community, which is something they have never done before. This means that Compound protocol developers would be able to run formal verification locally, understand what it’s doing, and potentially diagnose or patch any issues they may encounter. I think this is an important consideration for adopting such a new technology, and am really glad to see Certora moving in this direction. This is hopefully a step in the direction of them completely open-sourcing the technology, which is something I think would give the community a lot of confidence that investing into CVLs will have a minimum long-term value for the protocol. I also think it aligns with the spirit of development for the Compound protocol and decentralized finance overall.

In my opinion, continuous formal verification is a step towards more efficient governance. It would decrease risk for the protocol and give further insight to governance, which can inform decision making. It should be part of our complete strategy for maintaining the integrity of the protocol, and this proposal gets us a long way towards those goals.

8 Likes