CertiK (CTK) (created in 2017) is a Cybersecurity company, using cutting-edge Formal Verification technology on Smart contract and Blockchain. The CertiK platform is a multi-faceted security solution for Blockchain. Utilizing the Security Oracle, the CertiKShield reimbursement protocol, and the most secure Smart contract Programming language in existence, DeepSEA, they can ensure the security of Blockchain across the entire lifecycle, from development to post-deployment.
The CertiK Chain, a security-first, Dpskyos (Delegated-Proof-Of-Stake) Blockchain, acts as the bedrock for which the future of Blockchain security is built.
CertiK leads Blockchain security by pioneering the use of cutting-edge Formal Verification technology on Smart contract and Blockchain. Unlike traditional security audits, Formal Verification mathematically proves program correctness and hacker-resistance.
CertiK is a technology-led Blockchain security company founded by Computer Science professors from Yale University and Columbia University built to prove the security and correctness of Smart contract and Blockchain protocols.
CertiK, in partnership with grants from IBM and the Ethereum (ETH) Foundation, CertiK’s mission of every audit is to apply different approaches and detection methods, ranging from manual, static, and dynamic analysis, to ensure that projects are checked against known attacks and potential vulnerabilities. CertiK leverages a team of seasoned engineers and security auditors to apply testing methodologies and assessments to each project, in turn creating a more secure and robust software system
A Cross-chain Protocol with Security Scoring and Decentralized Reimbursements for Building Secure dApps and Blockchain
CertiK has served more than 100 clients with high-quality auditing and consulting services, ranging from stablecoins such as Binance’s BGBP and Paxos Gold to Decentralized oracles such as Band Protocol and Tellor. CertiK customizes its engineering tool kits while applying cutting-edge research on smart contracts, for each client on its project to offer a high-quality deliverable.
The CertiK platform is envisaged to be a formal verification framework for building fully trustworthy smart contacts and Blockchain ecosystems. Different from the traditional testing approaches to detect bugs, the CertiK platform attempts to mathematically prove that Blockchain ecosystems are bug-free. The Foundation has developed modular verification techniques to decompose such an otherwise prohibitive proof task into smaller ones that can be automatically solved in a decentralized style. These proof objects can be built and encoded in the CertiK platform’s transactions and will then be validated by other participants.
Thus, the CertiK platform’s Blockchain is intended to work as certificates to exhibit the end-to-end correctness and security of the verified Smart contract, libraries of Decentralized application (DApp), and the implementations of the Blockchain itself.
In April 2022, CertiK raised an additional $60 million in a funding round led by SoftBank Vision Fund 2 and Tiger Global. Since January 2017, the company has raised a total of $300.2 million in ten funding rounds led by various venture capital firms such as Binance Labs, Sequoia Capital, Advent International, Hillhouse Capital Group, and others.
Smart Contract Audits
Combine manual testing, static analysis, and formal verification for the most robust Smart contract security in the industry.
Integrate with CertiK’s formal verification proof engine to create a more scalable and secure ecosystem.
Leverage a world-class team of Cybersecurity experts to prevent critical attack vectors and vulnerabilities.
CertiK Core Advantages:
- Comprehensive and Customizable Formal Verification
- Detailed and Transparent Audit Reports
- Code Review by Security Experts
- Audits Performed Across All Major Protocols and Languages
- Auto-generated Counterexamples
- Unlimited Code Re-Audits
- Advanced Penetration Testing by Experienced and Ethical Hackers
Services Certik offer
Uses can Identify and eliminate security vulnerabilities using the most rigorous and thorough Cybersecurity techniques. Cetik security audit platform evaluates Smart contract for vulnerabilities and certifies their behavior with respect to a custom function specification.
The audit reports are custom, thorough, and transparent. The report will classify any identified vulnerabilities by severity (Critical, Medium, Low), along with suggested remediations. They also include user entire source code, with annotations and CertiK’s Formal Verification labels in-line to show their work and explain the mathematical proofs conducted.
Types of Audit Services:
- Crowdsale / Token Contracts
- Custom Smart contract
- Wallets and DApps
- Blockchain Protocols 
Certik Penetration Testing services uncover even the smallest weaknesses by leveraging proprietary tooling, powered by an experienced team of ethical hackers. It Expose weaknesses in users systems and IT infrastructure before they're exploited by hackers.
Custom Formal Verification:
Expand the capabilities and security of your platform by integrating with the core of our Formal Verification proof engine. For Blockchain protocols, CertiK provides customized solutions by performing Formal Verification for smart contracts and Decentralized application (dApp) developed on the platform, aiming to ensure a trustworthy Blockchain ecosystem and a prosperous Decentralized community
Type of Custom Formal Verification:
Customized Verification Solution : Receive an automated Formal Verification layer for your platform that can assist in identifying vulnerabilities in smart contracts within your Blockchain ecosystem .
- Exclusively built for your Blockchain platform
- Parses the front-end for your Smart contract language
- Adapts to the unique characteristics of users platform
Formal Verification of User Platform: Conduct rigorous verification to Audit users Blockchain platform and eliminate several critical vulnerabilities that may affect the specified user Blockchain ecosystem.
The CertiK Security Oracle:
The CertiK Security Oracle retrieves a set of security scores from a Decentralized network of security operators, who assess the reliability of source code and are rewarded in CTK, the native digital fuel of the CertiK Chain. The Security Oracle relays these assessments and combines them to create a real-time, on-chain aggregate score that can be used by anybody seeking to validate the security of the contract.
Depending on the risk tolerance of the interacting party — whether it’s a user or another smart contract — the security score can provide insight into whether transaction sizes should be smaller, split apart, or even stopped altogether. 
The Security Oracle retrieved a low security score, and the security check saved the user from losing their assets in this dangerous transaction.
The Security Oracle continuously aggregates the security assessments of a smart contract into the on-chain score — projects can get their code audited in an agile fashion to meet their aggressive timelines. By using a decentralized group of security operators, the suite of security primitives is constantly growing. New static analyzers and security tools can be created, and their assessments would also get incorporated into the ever-updating Security Oracle score.
A CertiKShield Pool is a Decentralized pool of CTK that is used to reimburse lost, stolen, or inaccessible assets from any Blockchain. The amount that’s lost can be reimbursed by the members of the CertiKShield Pool.
There are two parts of the CertiKShield system: 1) members who fill the pool with CTK as collateral to be used to reimburse approved Claim Proposals, and 2) members who seek to protect their crypto assets by reserving a part of the CertiKShield Pool.
CertiK Chain is designed to be the infrastructure of provable trust, for all stakeholders in the Blockchain world. Designed from ground up with Blockchain security in mind, CertiK Chain is a Proof-of-stake (PoS) Blockchain that prioritizes security and cross-chain compatibility.
Additionally, the chain is interoperable, meaning it can be utilized in conjunction with existing blockchains and smart contract platforms. CertiK Chain was built as a Cosmos Hub while maintaining full EVM compatibility, designing itself to not only co-exists with many other blockchains, but to have deep technical integrations and collaborations with them for stronger security across the space. CTK is the native digital utility fuel of CertiK Chain, serving as the core utility for the CertiK Security Oracle and CertiKShield.
DeepSEA is a secure Programming language and compiler toolchain developed by researchers from CertiK, Yale University, and Columbia University, vastly mitigates the security risks of smart contracts during the development process itself, prior to deployment. Developers can generate machine-checkable proof-objects while they code, easily proving the correctness of their output.
DeepSEA has been awarded research grants from the Ethereum Foundation, Columbia-IBM, and the Qtum Foundation to push forward its hyper-secure programming language.
CertiK Virtual Machine (CVM):
Perhaps the most well known virtual machine in Blockchain, the Ethereum Virtual Machine (EVM), serves as the processor for Ethereum Smart contract to be transformed into Bytecode and executed.
The CertiK Virtual Machine (CVM) is fully compatible with the EVM, but has been architected to follow the leading universal VM found in computers worldwide, the x86–64 OS process model, while potentially expanding to other ISAs such as arm64 in the future.
The CVM exposes smart contract and Blockchain security information, enabling unprecedented ways to access, check, depend on, and even dynamically establish Blockchain and Smart contract security.
CertiKOS for CertiK Chain:
CertiKOS is a certified, concurrent operating system kernel (the core of any OS) and hypervisor developed at Yale University, receiving international acclaim as the world’s first “hacker-resistant” OS kernel.
CertiKOS can be used as a replacement for Linux for certain mission-critical applications, such as the running of a CertiK Chain node or CertiK Security Oracle. By using CertiKOS instead of trusting the 27 million lines of Linux code, these simple, yet mission-critical operations may perform with less unnecessary risk of bugs.
Certik Skynet & Certik Security Leaderboard
In November 2021, Certik introduced Skynet, a security intelligence engine that constructs security insights for blockchain-based projects and smart contracts 24/7 for 365 days. It powers the security score on Certik's web3 Security leaderboard. It gathers and analyses big amounts of raw data both on-chain and off-chain using sets of machine learning and big data techstacks with security-based algorithms and ultimately produces it in the form of simplified metric like a security score. The Certik Skynet covers various aspects such as static code, on-chain metrics, social sentiments, governance and autonomy, market volatility, and security before producing a security score for the project. The Security Leaderboard is an attempt to make security metrics public, accessible, and transparent for all. The security score is upgraded to Skynet Trust Score in 2022. The CertiK Security Leaderboard provides an in-depth overview of the security of DeFi, Crypto, and Blockchain-based projects. In 2022, the Skynet badge and the KYC badge features were added, which increased visibility to the projects.
Certik On-Chain Governance
The on-chain governance of CertiK Chain upholds the core values of decentralization, transparency, and security.
- Stake Delegators: any CertiK Chain user who may delegate their CTK stakes to Validator Operators, entrust Security Certifiers with their votes, and vote directly on non-security-relevant governance proposals.
- Security Certifiers: a set of security experts who protect the chain by voting on all security-relevant governance proposals and all security-related chain activities.
- Validator Operators: a set of operators of CertiK Chain validator nodes who are responsible for chain operations, including block production and non-security-relevant governance by delegation.
Security Certifiers are unique to CertiK Chain. This group of security experts work to protect the chain by voting on all security-relevant governance proposals and all security-related chain activities.
Security Certifiers can be added and removed so long as there is sufficient agreement from the relevant parties, including Delegators, and Validator Operators.
Voting rights for both operational and financial aspects of the CertiK Chain are bestowed upon Validator Operators, the representatives of stake delegators.
Stake delegators, users who choose to stake their CTK to validators for rewards on the chain, are granted the ability to vote directly on non-security related governance proposals. Alternatively, delegators can choose to entrust Security Certifiers with their votes. 
Types of governance proposals include:
Plain Text Proposal: A proposal related to chain operations and governance prior to implementing on-chain modifications. Those wishing to create a Software Upgrade Proposal must first submit a Plain Text Proposal outlining the request.
Software Upgrade Proposal: A proposal to CertiK Chain code following a successful Plain Text Proposal.
Bounty Proposal: A proposal for a contribution request, including the performance of security verifications and security audits. The deposits for a bounty proposal are stored in a pool that can be claimed by contributors who complete the request.
Community Pool Spend Proposal: A proposal to transfer CTK from the Community Pool (more on that below) to a CertiK Chain user who has performed, or is set to perform, development or security work for the Chain.
Certifier Update Proposal: A proposal submitted by Security Certifiers when seeking to add or remove a Certifier.
CTK is the native digital fuel of the CertiK Chain. It is used to reimburse lost, stolen, or inaccessible assets from any Blockchain. The amount that’s lost can be reimbursed by the members of the CertiKShield Pool.
CTK has a total supply of 100,000,000 CTK. It recorded an all-time high of $1.94 USD on October 27, 2020, and an all-time low of $0 USD of October 23, 2020. CTK was created in October 2020.
Certik Partners and Listed Exchanges
Different from the traditional testing approaches, CertiK attempts to mathematically prove Blockchain ecosystem and smart contracts are hacker-resistant and bug-free. Trusted by the security industry, CertiK has established strategic partnerships with the world’s top digital asset exchanges, such as Binance, OKEx, KuCoin, and Huobi, as well as Blockchain protocols, such as NEO, ICON, and QuarkChain.
CertiK is an international company with team members around the world.
|Prof. Zhong Shao||Co-founder||Thomas L. Kempner Professor and Chair of Computer Science Department at Yale University. Ph.D. in Computer Science from Princeton University. Leading figure in research fields such as cybersecurity, operating systems, and certified software. Shao and his Yale FLINT group have developed the world’s first hacker-resistant and concurrent operating system – CertiKOS.|
|Prof. Ronghui Gu||Co-Founder||Tang Family Assistant Professor of Computer Science at Columbia University. Ph.D. in Computer Science from Yale University and Bachelor’s degree from Tsinghua University. Primary designer and developer of CertiKOS and SeKVM. Gu has received: an SOSP Best Paper Award, a CACM Research Highlight, and a Yale Distinguished Dissertation Award.|
|Dr. Zhaozhong Ni||Chief Technology Officer||Zhaozhong Ni was formerly an engineering lead at Google and HP / 3PAR and a researcher at Microsoft Research. He is an expert in systems software and formal verification and has extensive experience in building operating systems kernels and mission-critical enterprise systems. Dr. Ni was a founding member of gVisor, Google’s new security focused OS with cloud-scale production. He holds multiple patents on distributed storage systems. He obtained his BS from Tsinghua University and his PhD in Computer Science from Yale University.|
|Daryl Hok||Chief Operating Officer||Daryl Hok spearheaded Corporate Development at FiscalNote, a global machine-learning legal tech company, where he accelerated growth by completing 3 acquisitions in 12 months, including a $180M purchase from The Economist Group. He was also the Product Manager responsible for ideation and release of SaaS products, along with the development of the core data infrastructure. He obtained a dual BA in Economics and Psychology from Yale University, with concentrations centered around behavioral economics|
|Dr. Vilhelm Sjöberg||Sr. Principal Scientist||Vilhelm Sjöberg was a former associate research scientist at Yale University. He received his Ph.D. in Computer Science from the University of Pennsylvania in 2015. He is an industry-leading expert in software verification, programming languages, and type systems. His research is focusing on language support for layered verified systems like CertiKOS, and currently he is developing DeepSEA which is a language to write verified smart contracts. Dr. Sjöberg is the winner of 2016 ACM SIGPLAN John C. Reynolds Doctoral Dissertation Award|
|Muhan Zou||Chief Strategy Officer||Muhan Zou serves as the founding member of CertiK from company inception, where he contributes with both his engineering abilities and team leadership. Muhan has years of experience in designing and developing enterprise level SaaS products. Prior to joining, he worked as the engineering lead at Comcast to monetize large-scale ads and settop-box/linear raw data into business insights deliverables. He also worked at Oracle where he built the social cloud platform as a Full Stack Engineer after graduation at Yale University.|
|Zhenhua Cao||Software Architect||Zhenhua Cao is a veteran in designing and building enterprise software. He was a Principal Software Engineer in FreeWheel, a Comcast company that is known for its TV and digital video advertising platform serving large media companies across the globe. He led a few key projects in FreeWheel including UI framework overhauls and UI products unification. Prior to FreeWheel, he was the tech lead for Groupon China with focus on web performance and user experience, and the Co-founder of Gamepub, a twitter-like social network for online gamers.|
|Yu Chen||Head of China||Yu Chen was the former CTO at Taopaipai, the biggest platform for professional wedding photography in China. He later became the technical VP/CTO at the WD Group and YouLanW and managed the technical team of apps and O2O system to help millions of blue-collar workers find their jobs. As one of the very first iOS developers, he released 2 apps out of 300 on the first day of iOS AppStore and latered founded Teemsoft, Inc, a game development company with 100+ employees. He obtained his BS from Xi’an Jiao Tong University and his Master in Computer Science from Loyola University Chicago.|
|Georgios Delkos||Lead Security Engineer||Georgios brings two decades of hands experience with Asterisk/VoIP and distributed systems. Spent the last eight years working mainly with blockchain. Author of Pirl Guard a novel consensus expansion for ethereum based chain models mitigating 51% attacks.|
|Shaau Lam||Head of CertiKShield |
Did you find this article interesting?