Specification and model checking of BFT consensus by Matter Labs
In 2024, I was engaged by the Security Team at MatterLabs. They needed help in formally specifying and checking the properties of the new algorithm that was being designed by the Consensus Team....
Earlier this year, I was engaged by the Security Team at Matter Labs. They needed help in formally specifying and checking the properties of the new algorithm that was being designed by the Consensus Team. What intrigued me is that the Consensus Team had the experience of implementing BFT algorithms with their Era Consensus, but their new algorithm – called ChonkyBFT – existed only in Rust-like pseudo-code. So the team wanted to start with a formal specification before diving into a full-featured implementation. Since I had the experience in specification and model checking of the Tendermint consensus at Informal Systems, this seemed like a feasible task to me.
See all the details in the much longer blogpost.
We have published the research paper on ChonkyBFT.