An Introduction to Formal Verification

CertiK | Jun 10, 2019

Article's Poster

Formal Verification: The Future Of Blockchain Security

What is Formal Verification?

Formal Verification is the highly specialized process that CertiK uses to mathematically prove the security and correctness of blockchain smart contracts.

Unlike manual security checks, Formal Verification examines the entire code logic at-scale and mathematically ensures your program works only as it’s intended to. To do that, Formal Verification thoroughly checks your program by calculating it against every possible value for all variables.

Formal Verification attempts to prove or disprove that the intended algorithms, protocols, or business functionalities are working the way they’re supposed to be. Rather than depending on error-prone human judgment, mathematical systems can calculate against near-infinite scenarios. By applying rigorous and complete mathematical reasoning against code, Formal Verification goes wider and deeper than any human team can.

Since its inception in the late 1960s, Formal Verification has been used in hardware projects in the financial, scientific and military worlds, such as NASA’s Mars Rover. With the innovation of the blockchain network, CertiK is introducing it into critical software spaces.

Why Does It Matter?

As blockchain projects scale in both size and complexity, Formal Verification can secure these programs by being built on unequivocal, mathematical fact.

This is crucial across the software world, but especially for the blockchain ecosystem. Blockchain projects have decentralized systems, meaning that once their started, they can’t be stopped. This means that any errors or vulnerabilities can be exploited by bad actors to make permanent, immutable hacks.

Formal Verification enters as a platform-agnostic solution to this problem. The only consistent language across the world is math, and Formal Verification provides technical proof that’s transparent, comprehensive, fast and true.

Fortunately, this solution is applicable all throughout the landscape. Innovations that CertiK has made in Formal Verification has expanded the flexibility so that every blockchain project can gain access to a more precise and accurate assessment of risk. Because CertiK’s proprietary technology can translate across compatible platforms and languages, engineers and developers can get unparalleled mathematical support to protect their code.

The time needed to complete a Formal Verification audit is also radically different. Rather than manually reading through code, CertiK’s Formal Verification uses computer programs to compute every possible variable, providing full comprehensiveness and freeing up countless hours of work. And, in the case of problem discovery, the Formal Verification process can pinpoint exactly where the problems are — and how to fix them. After this computation, CertiK’s team of experts provide a full review of the code and mathematical outputs, efficiently combining both exhaustive computer review and thorough manual review.

Ultimately, Formal Verification provides a better security product for blockchain and smart contract companies, allowing them to focus on proving out their concept in practice, rather than worrying about security breaches.

Blockchain is next-generation technology. Shouldn’t it have next-generation security?

*****

To request an audit or verification of your smart contracts, please email audit@certik.org.

For more information, visit certik.org.