Introduction : What is CertiK and why this project is highly needed in the cryptocurrency space
Team, Partnerships and Funds
Usage
Competition and Development Roadmap
Conclusion
Useful links

1. Introduction

What is Certik ?

An awesome short presentation video

CertiK is a formal verification framework to mathematically prove that smart contracts and blockchain ecosystems are bug-free and hacker-resistant. To scale the verification, CertiK developed a layer-based approach to decompose such an otherwise prohibitive proof task into smaller ones. These smaller proof obligations can be encoded in the CertiK transactions and will then be proved and validated by the participants in a decentralized style. Thus, the CertiK ledgers work as certificates to exhibit the end-to-end correctness and security of the verified smart contracts and verified blockchain ecosystems, making them entirely trustworthy.
The CertiK team consists of world-class formal verification experts who are professors from Yale University and Columbia University, as well as senior software engineers from Google, Facebook, and FreeWheel.

Details:
Token Symbol: CTK
Crowdsale Token Price: TBA
Hard Cap: TBA
Total Tokens for Sale: 100,000,000
Crowdsale Date: TBA

The upcoming short video briefly explains how CertiK works. They even have demo video, which you will find later in this article.

Why is CertiK highly needed in the cryptocurrency space ?

As we know the blockchain is vulnerable, we are seeing more and more hackers targeting the cryptocurrency space. Further growth will only bring more exposure. There have been a lot of funds stolen and people lost entire fortunes. Yes, I know, investment is risky ! But why not make the space safer ? This way more people will gain the trust needed to invest in this new technological revolution, that is currently taking place in front of our eyes.

Let's start with how the cryptocurrency space evolved lately :

Blockchain implementations are error-prone : Ethereum virtual machine implementation has 703 open issues and 2186 closed issues (1/15/2018).

Smart contracts are open-sourced to hackers and immutable once deployed : TheDAO - 1 bug, 50$ million lost, fixed by hard fork.

Only in 2017 630 million $ have been lost to hackers in 12/2017.

This year we saw the Bancor issue that led to millions of funds lost. Certik could have helped warn Bancor and prevent this.

You can see how CertiK could have helped Bancor here

On June 16th 2018, a bug occurred in the ICON smart contract, this error was exploited by malicious actors to affect the functionality of the network. The bug couldn't be used for stealing tokens. Yet, Certik could help ICON fix the detect ICX EnableTokenTransfer Issue. I think they already did and are planning a lot of things together, because they just announced they partnership with ICON. You can see more about the issue here

2. Team, Partnerships and Funds

CertiK Team Leaders

Partnerships and Funds

CertiK has just started to announce their partnerships 1 month ago. The list of partners released one by one confirms that this project is not to be taken lightly, as it can be a game-changer. And I have a feeling that the list of partners is not yet complete. You can check their tweets to see what are their current partnerships and also for checking the upcoming ones. I have left all the useful links at the end of the article.

3. Usage

The Foundation behind the project has developed a one-stop solution, called the CertiK Platform, which provides a powerful and efficient set of Certified Kits for building fully trustworthy blockchain ecosystems. The Platform is comprised of:

Smart labelling :

The CertiK Platform has designed a labeling approach in order to specify dApps/systems. These labels are expressive enough to formally state the desired properties and are compatible with existing programming languages such as Solidity. Also, via the utilization of deep learning techniques with a manually established labelled code base for training, the CertiK Platform intends to introduce a smart labelling framework, to help understand decentralized programs at both the syntax and semantics levels, and then automatically add proper labels to the source code.

Layer-based decomposition :

The CertiK team is striving to achieve modular verification by realizing a named layered deep specification concept. This technique uncovers the insights of layered design patterns and makes it possible to break down a complex proof task into smaller ones, and verify each of them at their proper abstraction level.

Pluggable proof engine:

The smaller proof obligations are easier to untangle and can be solved by some automatic verifiers such as SMT solvers. To enable extensibility, the CertiK Platform is intended to provide an open protocol whereby significantly more advanced solving algorithms can be freely plugged into this system.

Machine-checkable proof objects :

The CertiK Platform constructs mechanized proof objects (or counterexamples) in such a way that these proofs can be quickly checked by anyone using their own machine. These proof objects can be viewed as the “certificates” to the verified programs.

Certified dApp libraries :

The CertiK Platform also offers a series of certified libraries and plug-ins to the integrated development environment (IDE) for building more trustworthy dApps. These libraries help improve the code quality and reliability of the entire blockchain community, and the use of these tools will cost a small amount of CTK as virtual crypto “fuel”.

Customized certification services :

For dApps/systems with high reliability requirements, such as digital wallets, the CertiK Platform intends to provide customized certification services. In such cases, verification experts will help specify/verify the programs and generate a detailed, comprehensive report.

CertiK system mainly involves 5 parties with each individual being assigned different tasks and roles to complete the system.

Customers : will be code developers or automatic programs that send codes to the system. The sent codes are called “Proof objects” and must be sent along with CertiK tokens (CTK) as a reward.
Bounty hunters : their tasks are to allocate computing resources to the system as well as to receive proof objects and to broadcast the works within the system. They are entitled to be rewarded with CTK tokens sent by the customers. To be qualified in this role, a certain party must possess a high number of CTK tokens as required by the system.
Checkers : their responsibilities are to record transactions or verify proof objects submitted by bounty hunters. Bounty hunters will receive the tokens when the checkers confirm the proof objects. Upon confirmation, the checkers will be rewarded with some CTKs.
Sages : will be connectors of proof engine to CertiK system. The proof engine is an algorithm deployed to find bugs in smart contracts. Sages will be rewarded based on performance of their engines. The bounty hunters will be users of proof engines
Users : this is suitable for developers who can link library of CertiK to IDE in order to create DApp. Users must pay expenses in CTKs. Users can subscribe to all CertiK Platform’s certified libraries and IDE plug-ins to build their own DApps/systems with some CTKs

These five roles will help to maintain the stability and sustainability of the CertiK ecosystem and can also lead to a natural growth in the importance and value of the CTK token.

CertiK makes use of its native CTK token which is used as a digital fuel across the platform. CTK is a non-refundable functional utility ‘fuel’ which will be used as the unit of exchange between participants on the CertiK Platform. CTK is also used in economic incentives which encourage participants to both contribute and maintain the ecosystem on the CertiK Platform. CTK acts as an integral part of the CertiK Platform, and provides a common unit of exchange that reward users and helps to keep the platform sustainable.

4. Competition and Development Roadmap

CertiK competitors are Quantstamp and Zeppelin.

Quantstamp system is based on manual checking. Altough Quantstamp has also planned to have automatic checking, according to CertiK's roadmap, they will be the first to launch the full system. Quantstamp's traditional system requires a large ammount of human effort in order to review the source code and manually write the specification.

Zeppelin uses the same manual checking system. Another negative aspect is that the libraries provided by them are either not verified or do not offer mechanized proof of objects.

The manual code review is inefficient, non scalable, takes a long time, and more importantly not so secure.

Development Roadmap

5. Conclusion

CertiK is a very interesting project because blockchain security is still a growing major problem. Smart contracts are very vulnerable and can create huge problems if the code isn't good. Investors need a safe environment in order to be able to trust projects with their money. Good security can also make institutional investors more likely to support the cryptocurrency space.

There's not to much competition in this field. If CertiK is able to deliver according to their roadmap, the project will certainly be a success. Taking in consideration their partnerships, I think that's inevitable.

CertiK is a real game changer and it's one of my top 3 upcoming favorite projects.

For a quick demo about code verification, please watch this video :