Granada has passed all three stages of voting and will be activated at the end of the Adoption period, which would likely take place this week on August 6. Liquidity Baking is one of the key features of Granada. We already wrote a first progress report on the verification of Liquidity Baking smart contracts in which we have provided an in-depth description of our effort to provide strong safety and correctness assurances. In this post, we would like to give a short update on our verification efforts around Liquidity Baking smart contracts.
In a nutshell, these efforts can be divided into two approaches: (1) formal verification of the CPMM contract using the Mi-Cho-Coq framework, and (2) intensive integration testing using property-based testing frameworks. Most notably, the tests implemented in (2) were focusing on the hypotheses used to conduct our formal proofs in (1). Recently, we have decided to increase the scope of our integration tests to also include some key properties proven in Coq using Mi-Cho-Coq. In particular, we are now testing that:
- All three balances of the CPMM contract are always strictly positive
- The CPMM invariant (see its definition here) is strictly increasing.
Having in our integration tests properties that have been proven in Coq may seem redundant but these tests will act as regression tests in case the CPMM contract is ever changed in future protocol update. Furthermore, it is reassuring to have results validated by two different methods.
Other audits and verification efforts
Speaking of different methods, we would also like to highlight that audits and verification efforts for Liquidity Baking smart contracts have been made outside of Nomadic.
Indeed an audit of tzBTC has been published in March 2020 by Least Authority.
Furthermore Runtime Verification have published a Formal Verification Report on Dexter 2 and have just released one on Liquidity Baking, which was based on the same contract.
Runtime Verification’s verification approach shares some similarities with our formal verification efforts with Mi-Cho-Coq. In both cases, the work relies on a formal semantics of Michelson (K-Michelson for Runtime Verification, Mi-Cho-Coq for Nomadic Labs) that permits to rigorously reason about the behavior of programs. Note also that similar properties have been proven (e.g., the functional correctness of the contracts’ Michelson bytecode, or the fact that the CPMM invariant is strictly increasing).
Of course, our approaches, while similar, differ in some aspects. In particular, Mi-Cho-Coq is based on Coq, while K-Michelson is based on the K Semantic Framework. We can also notice that the verification effort of Runtime Verification also covers the FA1.2 contract used by the CPMM to manage the tokens distributed to the liquidity providers. Overall, we believe that our approaches are complementary.
We are glad that several teams have independently studied the security of the Liquidity Baking contracts, as it gives the community more assurances that Liquidity Baking is safe to use.