Runtime Verification is excited to announce a new engagement with PlatON Networks, a privacy-protecting new generation of public chain sponsored by the LatticeX Foundation (Singapore)
PlatON was forked from Ethereum, reborn with a brand new consensus algorithm and PlatON POS (proof of stake). The focus of this engagement is the formal modeling of PlatON’s Concurrent Byzantine Fault Tolerance (CBFT) protocol and verification of two mission-critical properties – safety and liveness. The latter will likely be spread out over two different engagement phases.
“To say we are excited to engage with PlatON Networks is an understatement. We began conversations with their team in late 2019 about how and where our two companies could engage. Although we discussed various opportunities, including those related to writing and verifying programs written in web assembly (WASM), we eventually settled on protocol verification as a good place to start what will hopefully become a long-term collaboration and partnership.”
– Patrick MacKay, Runtime Verification’s Chief Operating Officer
CBFT is PlatON Network’s consensus protocol. It derives from several existing protocols, but also introduces new technologies that aim at improving efficiency and scalability of the network, including perhaps most importantly the concurrent production of blocks in one round.
As in other consensus protocols, two fundamental requirements ensuring the protocol’s security and proper operation are safety and liveness. Formally modeling the protocol and verifying these two properties provides a high level of assurance of correctness of the protocol’s design and enables making explicit all the assumptions under which the properties are satisfied.
