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.


CertiK Ecosystem


Strategic Investors