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]}