Project Spotlight – CertiK

(Certik, 2018)


The Certik platform is a framework that utilizes formal verification to build fully trustless smart contracts and certified blockchain ecosystems. With the goal of proving the blockchain ecosystems are mathematically bug-free, CertiK introduces modular verification techniques which decompose single proof tasks into smaller proof objects. These proof objects will be validated by the participants on the platform, and ultimately be solved in a decentralized way. The Certik ecosystem serves as certificates to the blockchain as they “exhibit the end-to-end correctness and security of the verified smart contracts, libraries of DApps, and the implementations of the blockchain itself ” (CertiK, 2018).

The Problems With Existing Verification Techniques

Blockchain Ecosystems Are Not Truly Trustless

Many seem to believe blockchain ecosystems are fully trustable and secure, but in fact they are very vulnerable as their protocol design and source code are generally exposed to the public. This opens the doors for malicious hackers to attack the projects and potentially walk away with lucrative profits (e.g. TheDAO hack). Even if the protocol is perfectly designed and bug-free, the ledger implementation might have flaws or not meet the specifications fully, which could make the project as a whole vulnerable.

In addition, cryptographic software libraries are fairly prone to errors. These errors can potentially lead to the digital signature mechanism being bypassed, which typically results in a huge economic cost. Lastly, it’s necessary to nate that fixing bugs on the blockchain is a rather long and slow process as any actions on the network need to reach consensus among the majority of nodes first.

Existing Verification Techniques Are Not Sufficient

Before verification techniques there was testing. Despite being widely used today to enhance the reliability and security of software, testing by itself does not “eliminate the zero-day vulnerability issues” (CertiK, 2018). Several existing verification techniques attempt to address such issues, but not without some limitations. See the table below.

The Solution — The CertiK Platfrom

In order to address the aforementioned problems, CertiK proposes a platform that 1) proves the functional correctness of programs, 2) scales the proof development by borrowing intelligence and computation resources from the community, 3) allows proofs to be validated locally, and 4) encourages people to participate in the validation process.

Certified kits

The platform provides a set of Certified Kits which consist of the followings:

  • Smart labeling: expressive labels used to specify DApps/systems. Not only do these labels formally state the desired properties, they are also compatible with most existing programming languages (e.g., Solidity). Most importantly, smart labeling is a framework that’s intended to understand decentralized programs on both syntax level and semantics level by utilizing deep learning.
  • Layer-based decomposition: a technique that “decomposes a complex proof task into smaller ones, and verifies each of them at their proper abstraction level” (CertiK, 2018).
  • Pluggable proof engine: an open protocol that enables the extensibility of the CertiK platform by allowing advanced solving algorithms to be freely plugged into the system.
  • Machine-checkable proof objects: mechanized proof objects (or counterexamples) to be checked by any individual machine; serve as the “certificates” to the verified programs.
  • Certified DApp libraries: “a series of certified libraries and plug-ins to the integrated development environment (IDE) for building more trustworthy DApps” (CertiK, 2018).
  • Customized certification services: premium certification services for fulfilling high reliability requirements in some DApps/systems.

The CTK Token

Used as the exchange unit between participants on the platform, the CTK token is a non-refundable functional utility fuel that incentivizes the participants to contribute to the ecosystem. In other words, the CTK token is “an integral and indispensable part of the CertiK platform” (CertiK, 2018).

Proof-of-Proof (PoP) Mining Scheme

CertiK introduces a new mining algorithm, named Proof-of-Proof (PoP), in which the mining difficulties are determined by the task of proof searching. PoP facilitates the process of solving concrete problems while contributing to the distribution of CTK tokens. Furthermore, PoP unifies the following five roles in the CertiK community through the flow of CTK tokens. In return, the five roles help balance and guard the CertiK community.

CertiK Technical Chain

CertiK Proof Engine

The main component of the CertiK proof engine is the compiler, the task of which is to compile labeled programs while parsing them into internal models for DApps. Not only are these internal models language independent (i.e. unified back-end), they also define how the system state consisting of global and local variables is changed by the DApps.

The CertiK proof engine facilitates a solving procedure done by randomly selected Satisfiability Modulo Theories (SMT) solvers. During this procedure, counterexamples (or hints) will be generated if problems are solved, and will also be checked with respect to proof obligations.

Layer-based Decomposition

As the name would suggest, Layer-based Decomposition is a layered approach that decomposes a complex system into smaller components. Such an approach helps sort and isolate the components, and as a result simplifies the environment model to be evaluated at each layer. A verification framework is also introduced by this approach, with the goal of modeling context contracts and context nodes in the environment model. All in all, the idea of implementing the Layer-based Decomposition approach is to make the components at each layer meet the layer specification, and ultimately prove the functional correctness of the whole system by linking the proofs together.



CertiK is an ambitious project with a team of formal verification experts and top software engineers behind it. The project provides a unique solution to the trust and security problems we experience in the blockchain space today, particularly in smart contracts. Comparing to existing verification service providers, CertiK offers their services at a significantly lower cost while covering a broader market. As profitable as the verification services are today, we believe Certik can lower the high entry to such services and eventually hit a trillion dollar market. All in all, we at Cypher Core believe CertiK is a solid long term investment.


[1] CertiK. (2018, May 3).CertiK Whitepaper[PDF].

[2] Formal Verification Platform for Smart Contracts and Blockchain Ecosystems. (n.d.). Retrieved from

[3] CertiK. (n.d.). Logo [Digital image]. Retrieved July 7, 2018, from×450.png

DISCLAIMER: This is not a sponsored. Information provided in this article does not constitute investment advice, financial advice, or any other sort of advice. You shall not treat any of the website’s content as such. Please do your own due diligence, and consult financial advisory before making any investment decisions. Cypher Core will not be held responsible for the investment decisions you make based on the information provided in this article.

Leave a Comment