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. CertiK ledgers work as certificates to exhibit the end-to-end correctness and security of verified smart contracts and verified blockchain ecosystems, making them entirely trustworthy.

Verification Service

  •   Smart Contract
  •   Platform Customization
Functional Correctness with Formal Verification
Specification Design
Implementation-Spec Equivalence Proof
Access Control Audit
Property Checking with Formal Verification
Integer Overflow
Buffer Overflow
Assertion Failure
Runtime Analysis
Deployment Testing
Unit Testing
Manual Review
Design Review
Gas Optimization
Use Case
Blockchain Platform Providers who need automated solutions for DApps and its ecosystems
An exclusive, customized product that fits platform-specific features into the CertiK Formal Verification Engine
We provide customized formal verification solutions to blockchain platform providers. Our programming language experts will work with your engineering team on the language/API design to make the platform safer and more robust to programming errors. We will integrate the platform-specific language with CertiK's core proof engine, allowing for scalable and machine-checkable application auditing just for your platform.

Strategic Partners

Team Leaders

Zhong Shao is Thomas L. Kempner Professor and Department Chair in the Department of Computer Science at Yale University. He earned his Ph.D. in Computer Science from Princeton University in 1994. During his early career, he was a key developer of the SML/NJ compiler and the main architect of its FLINT certifying infrastructure. In recent years, Shao has been a leading figure working on the highly visible research fields on cybersecurity, programming languages, operating systems, and certified software. He and his FLINT group at Yale have developed the world's first hacker-resistant concurrent operating system CertiKOS---a major milestone toward building cyber-physical systems that are provably free from software vulnerabilities. Shao is the author or co-author of 90 articles in top scientific journals and conferences.

Prof. Zhong Shao

Co-Founder, President

Ronghui Gu is a tenure-track Assistant Professor of Computer Science at Columbia University. He obtained his Ph.D. in Computer Science from Yale University in 2016, where his dissertation won the Distinction Dissertation Award at Yale and was nominated for the ACM Dissertation Award. He obtained his B.S. from Tsinghua University in 2011. Prof. Gu is an expert in formal verification of system software. He was the primary designer and developer of CertiKOS, the world's first fully verified concurrent OS kernel. His OSDI16 paper on CertiKOS has been nominated and selected for publication in the Research Highlights section of the CACM.

Prof. Ronghui Gu


Vilhelm Sjöberg is an associate research scientist at Yale University. He received his Ph.D. in Computer Science from the University of Pennsylvania in 2015. He is an expert in software verification, programming languages, and type systems. His thesis research focused on making dependent type systems more attractive for general purpose programming languages by making it optional to prove that functions terminate, and by incorporating automatic theorem proving via congruence closure. Currently he is interested in language support for layered verified systems like CertiKOS. Dr. Sjöberg is winner of 2016 ACM SIGPLAN John C. Reynolds Doctoral Dissertation Award.

Dr. Vilhelm Sjöberg

Principal Scientist