Since our inception as a company founded by two professors, we’ve grown tremendously. And as we come up to our official two-year anniversary, it’s safe to say we’ve accomplished a lot.
But first, let’s rewind time and understand how CertiK was built.
Our beginnings date back to 2015 when our co-founders, Dr. Zhong Shao and Dr. Ronghui Gu, researched the monumental impact of certified software through Formal Verification, yet realized the limitations caused by the difficulty associated with the methods. As a result, Formal Verification — with its benefits of providing mathematical assurances to prove correct software — had not yet successfully transitioned into mainstream applications. Notable applications were still most commonly associated with mission-critical hardware applications, like NASA’s Mars Rover and aerospace devices.
As Professors Shao and Gu dug deeper, they found that the primary limitation was caused by writing correct specifications, and not the actual computation of the proofs. Deep Specifications were their novel methods of decompose a very complex proof of obligations into many smaller and easier-to-solve ones. They discovered that once you can prove each sub-component, you could then assemble the proofs back to deliver an end-to-end, comprehensive review.
DeepSpec, which was a research effort between Yale, Columbia, MIT, Princeton, and UPenn, received funding from the National Science Foundation to further the groundbreaking research. In 2016, Deep Specifications were used to create CertiKOS, the world’s first fully verified, concurrent OS kernel and hypervisor (we’re even on the Wikipedia page for Formal Verification!). CertiKOS works as a military-grade enclave to run software programs securely and efficiently.
With the success of the DeepSpec techniques that created CertiKOS, Professor Shao and Professor Gu believed that the same technology could heavily impact the blockchain world and smart contracts. The DeepSpec technique makes it possible to decompose a complex proof task within a smart contract into smaller ones, while verifying each of them at their proper abstraction level.
Concurrently, CertiK is also advancing blockchain security from the inside-out by creating the DeepSEA functional programming language. DeepSEA allows source code, such as smart contracts, to run in the Coq interactive proof assistant, paving a way to generate and prove automated mathematical proofs.
CertiK was established in December 2017, and it has grown stronger ever since. Two years later, the company has performed over 200 audits, secured more than $6.23B worth of assets, hired a world class global team, continued development on CertiKOS and DeepSEA, and publicly launched the Testnet of the CertiK Chain!
As we reflect on our second year, we know that blockchain will continue to scale and evolve to better serve the needs of the people and programs involved. The promise of Formal Verification within the blockchain world is that anyone, whether they’re active participants in the blockchain ecosystem or not, can build, trade, and use the ecosystem with confidence.
And now for the fun stuff! Let’s celebrate! Follow us on Twitter to stay updated for our swag giveaway and other activities!
Thank you to everyone that has been supporting us on our journey to secure the blockchain world. We’re incredibly thankful and proud to have a group of supporters who strongly believe in our vision.
Let’s work to build secure systems, together.
Onward and upwards,
The CertiK Team
