Mooly Sagiv, also known as Shmuel Sagiv, is the the Chief Scientist at Certora, a company he co-founded to scale the application of formal verification in enhancing the security of smart contracts in the blockchain sector. ^{[1] [11]}

Early Life and Education

Mooly Sagiv was born in Israel and demonstrated an early aptitude for mathematics and computer science. He pursued his higher education at the Technion - Israel Institute of Technology, where he completed his Ph.D. in Computer Science in 1991. His doctoral research laid the groundwork for his future innovations in software verification. ^{[2] [11]}

Career

Academic Career

Mooly Sagiv began his academic career at Tel Aviv University, where he progressed from Lecturer to Full Professor. He serves as Chair of Software Systems and Professor at the Blavatnik School of Computer Science and AI at Tel Aviv University, a position he has held since April 1998, which served as a basis for later work with digital assets.

His research has focused on program analysis and software verification. His areas of study include static program analysis, shape analysis, abstract interpretation, logic, theorem proving, programming languages, formal methods, data-flow analysis, program slicing, network verification, and smart contracts. His most cited work addresses shape analysis through three-valued logic and was implemented in the TVLA system.

Sagiv’s publications examine subjects such as dataflow analysis, symbolic execution, and methods used to analyze and verify program behavior. His academic work has also involved research related to theorem proving and abstract interpretation.

From August 2006 to August 2007, Sagiv was a Visiting Professor at the University of California, Berkeley, in the Electrical Engineering and Computer Sciences (EECS) department. Between August 2008 and August 2010, he served as a Visiting Researcher at Stanford University.

A study of authorship and collaborations within the Programming Languages research community referred to Sagiv as “the Kevin Bacon of the PLDI community”.

IBM

Sagiv worked at IBM as a Team Leader between October 1990 and October 1993 in Haifa, Israel.

Certora

In 2018, Sagiv co-founded Certora, a company focused on the formal verification of smart contracts and blockchain-based software systems. He served as Chief Executive Officer from November 2018 until June 2025.

The company developed verification tools intended to analyze the behavior of smart contracts and software systems used in decentralized finance applications.

In June 2025, Sagiv assumed the role of Chief Scientist at Certora, based in the New York City Metropolitan Area.

His work at the company has involved the application of formal methods and software verification techniques to blockchain-related systems and smart contracts.

Collaborations and Professional Activities

Sagiv has participated in collaborative research projects related to programming languages and software engineering. His work includes collaborations involving program analysis and software verification.

He has also participated in conferences and symposiums related to computer science and software engineering, including the European Symposium on Programming (ESOP) and the International Conference on Software Engineering.

Awards and Recognition

Sagiv received the Wolf Foundation Fellowship in 1989 and the IBM Outstanding Technical Achievement Award in 1993. Between 2000 and 2005, he received IBM Faculty Awards.

In 2002, he received the Friedrich Wilhelm Bessel Research Award.

In 2011, Sagiv received the ACM SIGSOFT Retrospective Impact Paper Award together with Thomas Reps, Susan Horowitz, and Genevieve Rosay.

In 2016, he received the Microsoft Outstanding Collaborator Award and was named an ACM Fellow.

His work in software engineering, program analysis, and formal methods has been referenced through academic awards, research collaborations, and positions in academia and industry. ^{[1] [2] [3] [4] [5] [6] [7] [8] [9] [10] [11]}

Interviews

Smart Contract Analysis at Fintech Symposium 2019 #01

On July 15, 2019, Mooly Sagiv presented the keynote talk “Modularity for Accurate Static Analysis of Smart Contracts” at the Fintech Symposium 2019, hosted by the YouTube channel “Datalogisk Institut - Københavns Universitet.”

During the presentation, Sagiv discussed methods for static analysis of smart contracts, with a focus on techniques intended to identify software vulnerabilities and verify specific program properties prior to deployment. He stated that some existing industrial analysis tools may produce false positives or fail to detect certain errors due to limitations in analytical precision.

Sagiv described an approach referred to as accurate static analysis (ASA), which operates on Ethereum Virtual Machine (EVM) bytecode rather than source code. According to the presentation, this method allows contracts to be analyzed even when source files are unavailable.

The talk also addressed modular verification methods designed to evaluate contracts in relation to the expected behavior of external contracts and system requirements. Additional topics included formal specifications, reentrancy vulnerabilities, financial logic conditions, and the use of automated verification procedures within smart contract development workflows. ^[12]

ETHGlobal Workshop on Formal Verification #02

On October 18, 2022, Mooly Sagiv participated in a workshop hosted on the ETHGlobal YouTube channel titled “Effective Code Security Tools.” During the session, he discussed challenges associated with smart contract security analysis, including false positives and undetected vulnerabilities in existing auditing and static analysis tools.

In the presentation, Sagiv described formal verification as a method that combines smart contract code with mathematical specifications intended to define expected system behavior. He explained that Certora’s verification framework analyzes compiled EVM bytecode in order to evaluate whether predefined conditions and invariants are preserved during execution.

The workshop included examples related to decentralized finance (DeFi) protocols and automated market makers. Sagiv stated that specification-based verification can be used to identify cases involving solvency conditions, invariant violations, and edge-case execution scenarios. He also described formal verification as a process that can be used alongside manual auditing, fuzz testing, and other security review methods.

The session further addressed the role of formal specifications in software development workflows. Sagiv noted that verification processes are more effective when integrated throughout development rather than applied only during later-stage audits. ^[13]