CertiK is a formal verification platform for building trustworthy smart contracts and blockchain implementations that aims to find flaws in entire blockchain implementations, cryptographic software libraries, smart contracts, and decentralized applications. A user will first upload code to the network and submit a proof request transaction. CertiK’s labelling software and in-house deep learning technology will label syntax and semantics of the code to capture exactly what the intended functionality of the code is. These labels will allow for uniformly deconstructing the program into multiple layers to turn large complex tasks into smaller mathematical equations then verifies them individually. Bounty hunters then verify these programs through multiple methods to ensure the code cannot produce a state that is inconsistent with the initially defined specification parameters. What comes of this interaction is turned into a certifiable proof object, which is uploaded to the network and verified by validators. While the proof engine will initially be powered by whatever solving algorithm is supplied by CertiK, the network will allow for sages to propose other more advanced proof engine frameworks for bounty hunters to adopt. CertiK’s platform will offer ‘full audit’ certification services that allows users to pay technical experts to provide detailed and comprehensive reports on programs with high-reliability needs. In addition, CertiK will provide ever-growing trusted code libraries and plugins that developers can use for a small fee in CTK. As well, entire applications can be created in the future using CertiK’s integrated development environment.
CertiK Strengths and Opportunities
CertiK is founded by renowned formal verification field experts Zhong Shao and Ronghui Gu, who developed the world’s first ever fully-verified operating system kernel that was verified using their proprietary methodology two years ago. This iterates a good demonstration of knowledge and understanding of the space that they are targeting. Unlike Quantstamp which is limited to EVM bytecode, CertiK will verify programs coming from multiple distinct chains. CertiK also aims to audit entire blockchain implementations and deal with state explosion problems. CertiK claims to have privately launched an alpha that is being used among 30 unknown commercial clients.
CertiK Weaknesses and Threats
CertiK faces competition from many protocols that have become industry standards at this point. One of which is Quantstamp. Quantstamp has heavy backing from the Ethereum and Wanchain community; was used to audit Plasma, Zilliqa’s sharding implementation, every single ERC-20 on Binance; and is partnered with multiple universities that will inform the Quantstamp network on new vulnerabilities that they discover in their research. The effectiveness of smart labelling and how CertiK will deal with state explosion problems in blockchain implementation verifications both depend on the CertiK team’s patented, unreleased technology. The labelling process poses it’s own vector of scalability concerns; the practicality of the network depends on smart labelling (no information on it out yet) as well as CertiK labelling, a library developed by experts on the network and the team. CertiK currently does not ensure functional correctness in it’s automated audit process.
Verdict on CertiK
CertiK sells itself in a very misleading way. The team contrasts their project with Quantstamp by claiming that in CertiK, everything is automated. However; human effort will still be needed in identifying labels, so the security loopholes present in Quantstamp that they claim to fill are presented as a result. With the entire system being based upon a labelling system that is based on a library of labels contributed by the team and experts participating in the network, CertiK is not too different at all from it’s competitors, if not worse. The CertiK project is unimpressive to me. I do not like the CertiK project or the CertiK token.
