Certora Chief Scientist Mooly Sagiv: Blockchain Security is More Than Just Code
What are the biggest security threats facing crypto in 2026?
- Published:
- Edited:
If 2025 taught us anything, it was that Solana hit breakout velocity and established itself as “the retail chain. Every day, thousands of users move funds and sign transactions, engaging with unfathomably complex smart contracts without a care for the potential risks.
Of course, the risks are still there underneath the service. But while crypto hacks and exploits are still far more common than we would like, people commonly assume that the biggest risks are buried deep in obscure logic and technical codebases.
Mooly Sagiv isn’t so sure.
According to the Chief Scientist of Certora, a blockchain security firm securing over $190B in DeFi TVL, most losses aren’t caused by faults in code logic or programming errors, but by far simpler culprits: Keys, custody, and human error.
“Keep an eye on your key… and keep an eye on your phone.”
It’s a simple warning, but it captures a critically important and often overlooked approach to crypto security. Security failures are rarely “just a bug”, and the proliferation of mobile crypto apps only adds more variables and potential vulnerabilities.
Sagiv is uniquely positioned to make that case. Known amongst his academic peers as Shmuel (Mooly) Sagiv, the Certora Chief Scientist has also served as Tel Aviv University’s Chair of Software Systems for almost 28 years. With decades of research in program analysis and verification, Sagiv plays a leading role in Certora’s push to scale formal verification beyond a niche discipline into something developers can run continuously.
Speaking with SolanaFloor at Breakpoint 2025, Mooly Sagiv cast an illuminating light into the dark forest of blockchain security. Responsible for auditing some of the biggest names in DeFi, Certora’s Chief Scientist broke down some of the biggest misconceptions crypto users have about security, the importance of formal verification, and whether AI and quantum computing risks are overblown.
Crypto Security’s Biggest Misconception: “All the Bugs Are in the Code”
When it comes to misconceptions about blockchain security, Sagiv argues that crypto culture is far too lax. The most dangerous misunderstanding is the belief that vulnerabilities live exclusively in code and that if the code is audited, users can abolish common sense.
“Everybody feels that all the bug[s] are in the code. And it’s not necessarily the case… maybe your code is perfectly fine, but there will be something outside… the way it’s deployed…”
Crypto folk stand by core philosophical tenets like ‘code is law’. But while that may be true, there are still dozens of variables that need to be considered. A protocol can be “correct” and still be unsafe because the keys are poorly controlled, the integrations are porous, or the operational environment is compromised. An app is only as secure as the systems and behaviours of the people managing it.
Sagiv’s second misconception is the one most users want to believe: that “audited” implies safety.
“It’s never fully safe. We can make it safer… but it’s never fully safe.”
Audits are undoubtedly an integral part of crypto security, but they’re by no means a guarantee. People develop a false sense of security once they see that an app has been audited, but DeFi users certainly shouldn’t forget basic security practices.
Certora’s Hybrid Approach to Security
Sagiv doesn’t dismiss audits. In fact, he explicitly argues against the idea that formal verification replaces human review. Instead, formal verification and human audits should ideally be used in tandem to provide as much coverage as possible.
Speaking with SolanaFloor, Sagiv outlined how audits typically defend against known attack patterns, while formal verification can reduce exposure to “unknown unknowns.”
“When you’re doing audit, you are reviewing your code [with] your best person against the known attack. When you are able to do formal verification… you have some kind of [prevention] of unknown unknown[s].”
That difference matters because crypto is an arms race. Attack techniques evolve, and hackers and cybercriminals are always finding new methods and techniques to break the billion-dollar apps we all use every day.
Whole new classes of bugs get discovered because someone, somewhere, found a clever way to break assumptions the industry didn’t even realize it was making. Formal verification aims to provide another line of defense against these “unknown unknowns”.
Sagiv describes a pattern Certora has seen repeatedly. Teams can do everything “right”, committing tremendous internal resources to security, hiring elite auditors, and then formal verification still surfaces additional high-severity issues.
“You let the best security [researcher]… find 10 critical. You’re very happy. And then you run formal verification. It finds two more.”
This thesis was further reinforced by Certora’s Formal Verification Team Lead Pamina Georgiev, who took the stage at Solana Breakpoint to illustrate the importance and impact of FV.
Despite all the promise and protection that formal verification offers, it’s still far from a perfect system. Formal verification is hardly an impenetrable force field that stops hackers in their tracks, despite what certain pockets of crypto Twitter might have you believe.
Sagiv is blunt about why that framing is dangerous.
“The biggest problem [in] formal verification is understanding what property to [specify]”.
Formal verification doesn’t prove the code is safe in some absolute sense. It proves that the code satisfies a set of properties; properties you asked it to prove. If you pick the wrong properties, you end up with something that looks extremely credible but far from watertight.
CI, Automation, and “No Human in the Loop”
One of Sagiv’s clearest points at Breakpoint is that security is not a one-time event. It’s not because an application got one audit several years ago that it will still be safe today. This is especially true in crypto, where protocols and attack methods iterate constantly and changes to a single line of code can have repercussions elsewhere in the stack.
“It completely changes, one change of one line can break the whole code.”
That’s why Certora pushes verification into the developer workflow. Sagiv says Certora integrates into CI pipelines, so each new commit triggers verification checks automatically, establishing a continuous guardrail rather than a one-off milestone.
“Every time they change, they do a commit in the code, we run formal verification. That's actually the beauty of our tool. Our tool is automatic; the human is not in the loop.”
Certora maintains dedicated documentation for formal verification of Solana programs, with the “Certora Solana Prover” designed to verify Solana smart contracts written in Rust.
Cypherpunks & Academia
Unlike many crypto origin stories, which are often rooted in a cypherpunk, anti-establishment ethos, Sagiv brings some much-needed academic class to the industry. He describes his transition from academia as a collision between intellectual challenge and real-world stakes.
“Crypto is the only domain where you have small code carrying a lot of value”
In traditional safety-critical software, the code might be massive, but it’s often old, stable, and the complete antithesis of crypto’s rapid iteration. This may have served as the basis for one of Certora’s favorite taglines: “Move fast and break nothing”
Sagiv frames crypto as a perfect fit for formal methods because so much of it is inherently mathematical: balances, invariants, conservation constraints, access control rules, and state transitions that can be expressed precisely.
“I give academic lectures still. Some people don't like the crypto. I try to motivate them on the technical side. I go back to the technical, and I'm telling them what is challenging.”
Even if his academic colleagues are skeptical of crypto, Sagiv emphasizes that crypto is one of the more stimulating and motivating areas of computer science for emerging developers.
Solana’s “Can-Do Attitude”
Certora is by no means a Solana-exclusive security firm, but that doesn’t mean that the company isn’t deeply intertwined in the chain’s DeFi scene. Having worked with some of Solana’s biggest and most influential applications, Sagiv affords the ecosystem a level of operational respect that only comes from brushing shoulders with top teams.
Certora’s first Solana engagement was with Squads, who Sagiv calls “amazing.” From there, Certora worked with the Solana Foundation and verified properties of SPL programs, describing the collaboration as unusually receptive.
What stands out most is his comparison to other environments. Touching on his experience with Solidity Developers, Sagic noted that teams can be resistant to changes.
“When we talk to people, sometimes in Solidity, ask them to change code they are very reluctant. They say we have a limited amount of time… Here [Solana] people have more of a ‘can do’ attitude. You ask them to change the code, they are very straightforward.”
Security Threats in 2026
When asked about the biggest threats that people need to be aware of in 2026, Sagiv once again highlighted that people shouldn’t over-index on code vulnerabilities. Good operational security is a multifaceted beast, and the average crypto holder is far more likely to find themselves a victim of social engineering or a custody error than losing funds in a DeFi exploit.
“We are seeing all kinds of things happening, it’s not just the code.”
He’s not wrong. According to Chainalysis’ 2025 Crypto Crime Report, fraudsters stole over $14B over the course of 2025 in yet another record high.
Sagiv also believes that the AI threat might be getting blown out of proportion. As you might expect from a security professional, Certora’s Chief Scientist considers AI not to be a malicious menace, but a tool. Granted, AI can serve as a multiplier for attackers, but it can also be leveraged by defenders and security firms.
“The bad guys could use AI. The good guys could use AI,”
If AI helps find vulnerabilities, it can also help prove properties, generate stronger specifications, and solve verification problems.
Crypto will never be “fully safe,” and Solana won’t be immune to whatever the next wave of attackers invents. But the path forward remains true to Crypto Security 101: Tighten key management, use common sense, and treat security as something you continuously prove, not something you declare once and forget.
Read More on SolanaFloor
The only certainty is uncertainty.
SolanaFloor Sits Down with Certora’s Mooly Sagiv
