CertiK CEO on securing Web3, the AI Agent threat, and why formal verification is the future of finance

As global finance rapidly migrates onchain, institutional investors face a terrifying reality where a single line of compromised code can vaporise hundreds of millions of dollars in seconds. Traditional security testing is no longer sufficient to build unshakeable trust.

In this interview, Ronghui explains how mathematical formal verification delivers the absolute certainty that financial institutions demand. He also outlines the hidden dangers of autonomous AI agents and reveals why operational security is now the most critical battleground in crypto.

Read more about his vision for a mathematically secure financial future below.

CertiK was founded in 2017 by professors from Yale and Columbia. What was the original idea, and how different is the company today from what you first wanted to build?

The name came from CertiKOS, a research breakthrough that Professor Zhong Shao and I made in 2016 at Yale and Columbia. We used formal verification to verify an OS kernel. It was supported by DARPA and used in a machine called LandShark. It was the first fully verified multiprocessor kernel designed to be hacker-resistant and bug-free.

In 2016, the DAO attack caused massive financial losses across the ecosystem. People quickly realised that this new blockchain stack required advanced security technology. The Ethereum Foundation provided a grant, and Binance became our first investor in 2017.

We grew incredibly fast, gained massive market share during DeFi Summer, and became a unicorn in 2021. Looking back, our academic background and research results gave us strong early technical advantages.

Backing from Binance, Coinbase, and major VCs such as Sequoia also helped us build critical trust and brand credibility in those early days.

During DeFi Summer, CertiK quickly utilised our technology to build a service that could scale to meet the massive demand for auditing. There were so many projects waiting months for audits, and that rapid pace also left us with some legacy issues.

When projects got hacked, people would often blame the auditors. That was never how things worked in any other industry, but the market was very immature at the time, and retail investors had unrealistic expectations.

CertiK has built relationships with regulators in the US, Singapore, Hong Kong, Japan, Abu Dhabi, and Korea. How have these discussions regarding blockchain security and regulation changed over time?

I would broaden this beyond cybersecurity to address the regulatory landscape as a whole. CertiK grew rapidly in 2021 and 2022, and I felt a profound responsibility to make a meaningful contribution to the industry. The most important step was advancing compliance and regulatory frameworks.

Starting in 2023, I began meeting regulators frequently. I served on the Hong Kong Web3 Task Force and as a technical advisor to the Monetary Authority of Singapore. Much of that early engagement took place in Asia and the UAE, as the US was not particularly crypto-friendly at the time.

One notable example is the recent issuance of Hong Kong's first two stablecoin licences. From the outside, it may look like a sudden development. In reality, we began pushing those initiatives three years ago. I flew back and forth between Columbia University and Hong Kong voluntarily to quietly help build those frameworks.

Many companies did similar unglamorous work behind the scenes to advance the industry. Now, the US environment has shifted considerably, and we are actively re-engaging with American regulators. We have submitted and had comments accepted, and we hope to keep pushing things forward globally.

At Paris Blockchain Week, you discuss how formal verification is becoming important for institutional trust. What do financial institutions need today before putting money into digital asset systems? And how much of that depends on a security audit versus a mathematical proof?

Institutional clients require an entirely different standard for code auditing. Professor Shao and I have spent decades in the field of formal verification. When we started CertiK, the industry was hesitant to pay for formal verification because it costs more than manual auditing.

That hesitation vanished late last year. People now fully accept that formal verification uses mathematics to prove properties of code. Testing can only prove that bugs exist, whereas formal verification is the only way to guarantee a system is truly bug-free.

Furthermore, a massive portion of today's code is generated by AI. You can use AI to review it, but nobody fully understands what happens inside those models. Projects are investing hundreds of millions of dollars in opaque code. Formal verification is the only credible way to provide guarantees for AI-generated smart contracts.

We are releasing a tool called Sparkle that uses AI to make formal verification highly cost-efficient and scalable for institutional clients. It is built on our research results called SPOCK and SPARK, which recently won the Best Paper Honourable Mention at SP.

In your PBW session, you also explain how Web3 security is evolving to meet the needs of global finance. Where is it already strong and reliable, and where is it still weak in a way that could worry large investors?

We see risks across many different layers. For years, the industry has focused heavily on smart contract security and allocated massive budgets to it. If you look at financial losses today, smart contract vulnerabilities are no longer the leading cause. Smart contracts have become highly secure.

The new critical weakness lies in operational security, specifically in private key management and the security of the entire operational stack. We saw this in recent high-profile hacks, where multisignature wallets were used, yet a key developer's device was somehow compromised.

Institutions find this terrifying. A traditional bank understands how to protect keys, yet they often lack awareness of the specific risks in Web3 environments. I know of a financial company that lost $50 million because a key developer left a backdoor in their system. In traditional finance, a scenario like that is almost unimaginable.

We must work with institutions to help them understand these risks, promptly recognise incidents, and build robust mitigation frameworks.

Your AI Auditor is constantly updated with real-world attacks rather than relying on fixed training data. How do you keep it up to date in an environment that moves as fast as AI and Web3?

AI models are developing incredibly fast. Each new version shows a massive leap in cybersecurity capabilities. I believe we are very close to the day when a language model can function independently as a senior security researcher.

However, all AI models are trained on data with a strict knowledge cutoff. To address this, we built an internal system called AirFlow, which powers our external AI Auditor.

We encode a vast amount of security research expertise, real-time vulnerability data, and bug databases into structured skills. This continuous context enhancement keeps the underlying model perfectly up to date.

Another major challenge involves balancing sensitivity and noise. If you configure a model to detect deep vulnerabilities, it generates false positives. If you reduce the noise too much, it misses useful findings. We spent a lot of time perfecting that balance by using multiple layers of detectors and validators to preserve the real findings while filtering out noise.

AI Auditor achieved an 88.6% detection rate across 35 real-world security cases. You said the real question is no longer whether AI can find issues, but which ones matter most. So where does the remaining 11.4% come from?

Achieving the perfect balance requires trade-offs. If we let the model run for ten hours instead of one, the results will change significantly. When we optimise for usefulness and efficiency, some findings will inevitably slip through.

Additionally, the AI models we use today are still catching up to the best human security researchers. Some vulnerabilities cannot yet be detected, or are only caught when the model is trained on a nearly identical case. If the underlying logic matches but the implementation looks different, the model might miss them entirely.

The goal of the AI Auditor is to be deeply integrated into the development cycle. It provides clients and institutions with immediate, low-cost feedback on their code before a formal audit even begins.

CertiK’s Open Cloud report showed that a trust model built for small environments failed when deployed at scale. Do you see the same problem across the wider AI agent ecosystem?

Yes. Most AI agent systems today share a very similar set of pain points. The prevailing design philosophy gives the AI agent access to everything it needs to assist you. Open Cloud became popular precisely because it had extensive access and could act autonomously.

That level of access creates significant vulnerability. Your system likely contains zero-day vulnerabilities in software like Slack or your email client. An attacker can use a zero-day exploit to compromise the AI agent and instantly take over your entire system. It is an extremely dangerous setup.

AI agents must be designed to operate in strictly sandboxed environments where all interactions are actively monitored. We also need dedicated security software running alongside the AI agent to detect and prevent malicious behaviour instantly.

Open Cloud introduced new types of risks, such as prompt injection, malicious tools, and privilege escalation. How different is auditing an autonomous AI agent from auditing a smart contract?

I divide this into three distinct categories: auditing smart contracts, auditing skills, and auditing AI agents. Auditing skills is actually easier than auditing smart contracts. Skills are written in plain text. While there are tricks for embedding malicious binaries in plain-text files, the process remains highly tractable. We are releasing a skill scanner very soon to address this.

Smart contract auditing is complicated because the vulnerabilities are deeply counterintuitive. However, the code is completely static. It never changes after deployment, and we have built excellent tooling for it over the years.

Auditing AI agents is genuinely difficult. Their behaviour is highly dynamic and completely non-deterministic. If you ask a model the same question twice, you will likely get different answers. Auditing for malicious behaviour that only emerges under specific conditions is a major challenge.

Furthermore, the attack surface is enormous. A smart contract manages specific assets within a defined scope, whereas an AI agent might have access to your entire workflow, emails, and files. Any weak point can compromise the entire protection layer. We contribute to AI agent security, but we do not yet have full confidence in it.

As AI is now used both to attack and to defend Web3 systems, how is CertiK’s role evolving? And what does a strong, mature security layer look like for a global Web3 financial system?

Attackers will absolutely use powerful AI models to their advantage. A hacker can let a model run for a hundred hours against a single target because the potential financial gain is enormous. Web3 security firms serving hundreds of clients simply cannot match that level of token spend on every single piece of code.

The playing field is somewhat uneven at present. We address this by encouraging clients to use formal verification for their smart contracts, where high stakes demand mathematical guarantees. We also strongly encourage all clients to continuously integrate the AI Auditor into their development cycles.

Using it throughout the entire lifecycle gradually accumulates AI-checking time, which helps level the playing field. Finally, attackers use AI for broad penetration testing, operational targeting, and social engineering. Companies absolutely must expand their security budgets beyond smart contracts to cover operational security holistically.