{"id":"mooly-sagiv","title":"Mooly Sagiv","content":"**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](https://iq.wiki/wiki/smart-contract) in the blockchain sector. [\\[1\\]](#cite-id-FgmgJZygNQOBq8qP)  [\\[11\\]](#cite-id-r8eOFTRqd7j8Yu2e) \n\n[YOUTUBE@VID](https://youtube.com/watch?v=1KR0GnxhNz4)\n\n## Early Life and Education\n\nMooly 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\\]](#cite-id-oO3vr8TMH04BC0en)  [\\[11\\]](#cite-id-r8eOFTRqd7j8Yu2e) \n\n## Career\n\n### Academic Career\n\nMooly 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](https://iq.wiki/wiki/digital-assets).\n\nHis 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.\n\nSagiv’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.\n\nFrom 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.\n\nA study of authorship and collaborations within the Programming Languages research community referred to Sagiv as “the Kevin Bacon of the PLDI community”.\n\n### IBM\n\nSagiv worked at IBM as a Team Leader between October 1990 and October 1993 in Haifa, Israel.\n\n### Certora\n\nIn 2018, Sagiv co-founded Certora, a company focused on the formal verification of [smart contracts](https://iq.wiki/wiki/smart-contract) and blockchain-based software systems. He served as Chief Executive Officer from November 2018 until June 2025.\n\nThe company developed verification tools intended to analyze the behavior of smart contracts and software systems used in [decentralized finance](https://iq.wiki/wiki/defi) applications.\n\nIn June 2025, Sagiv assumed the role of Chief Scientist at Certora, based in the New York City Metropolitan Area.\n\nHis work at the company has involved the application of formal methods and software verification techniques to blockchain-related systems and [smart contracts](https://iq.wiki/wiki/smart-contract).\n\n### Collaborations and Professional Activities\n\nSagiv has participated in collaborative research projects related to programming languages and software engineering. His work includes collaborations involving program analysis and software verification.\n\nHe 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.\n\n### Awards and Recognition\n\nSagiv 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.\n\nIn 2002, he received the Friedrich Wilhelm Bessel Research Award.\n\nIn 2011, Sagiv received the ACM SIGSOFT Retrospective Impact Paper Award together with Thomas Reps, Susan Horowitz, and Genevieve Rosay.\n\nIn 2016, he received the Microsoft Outstanding Collaborator Award and was named an ACM Fellow.\n\nHis work in software engineering, program analysis, and formal methods has been referenced through academic awards, research collaborations, and positions in academia and industry. [\\[1\\]](#cite-id-FgmgJZygNQOBq8qP)  [\\[2\\]](#cite-id-oO3vr8TMH04BC0en)  [\\[3\\]](#cite-id-iXCJglOBf7JbqtZI)  [\\[4\\]](#cite-id-bgyXbu14o9XEmLnd)  [\\[5\\]](#cite-id-oJg7rCGrknQ4Pw1p)  [\\[6\\]](#cite-id-p3NTtwHsu0ADUPH9)  [\\[7\\]](#cite-id-j6TEO1NDnfGSPhjq)  [\\[8\\]](#cite-id-01P3TYAt3xCDMWN0)  [\\[9\\]](#cite-id-iZ4A6WORLyAM5ndD)  [\\[10\\]](#cite-id-TJa4Awx719EMWaF9)  [\\[11\\]](#cite-id-r8eOFTRqd7j8Yu2e) \n\n## Interviews\n\n### Smart Contract Analysis at Fintech Symposium 2019 #01\n\nOn July 15, 2019, Mooly Sagiv presented the keynote talk “Modularity for Accurate Static Analysis of [Smart Contracts](https://iq.wiki/wiki/smart-contract)” at the Fintech Symposium 2019, hosted by the YouTube channel “Datalogisk Institut - Københavns Universitet.”\n\n[YOUTUBE@VID](https://youtube.com/watch?v=R3NP5cA5FVU)\n\nDuring 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.\n\nSagiv described an approach referred to as accurate static analysis (ASA), which operates on [Ethereum Virtual Machine](https://iq.wiki/wiki/ethereum-virtual-machine-evm) (EVM) bytecode rather than source code. According to the presentation, this method allows contracts to be analyzed even when source files are unavailable.\n\nThe 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](https://iq.wiki/wiki/smart-contract) development workflows. [\\[12\\]](#cite-id-lKwO7E7mMbSjJUor) \n\n### ETHGlobal Workshop on Formal Verification #02\n\nOn October 18, 2022, Mooly Sagiv participated in a workshop hosted on the [ETHGlobal](https://iq.wiki/wiki/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.\n\n[YOUTUBE@VID](https://youtube.com/watch?v=2fPTV8VLow8)\n\nIn the presentation, Sagiv described formal verification as a method that combines [smart contract](https://iq.wiki/wiki/smart-contract) code with mathematical specifications intended to define expected system behavior. He explained that Certora’s verification framework analyzes compiled [EVM](https://iq.wiki/wiki/ethereum-virtual-machine-evm) bytecode in order to evaluate whether predefined conditions and invariants are preserved during execution.\n\nThe workshop included examples related to [decentralized finance](https://iq.wiki/wiki/defi) (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.\n\nThe 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\\]](#cite-id-iF5fYg2yW5QjSpZY) ","summary":"Mooly Sagiv is an influential computer scientist known for his work in formal verification, program analysis, and smart contract security, currently serving as Chief Scientist at Certora.","images":[{"id":"QmUXX3ggHaunjc7BEha3JGTKpFAfDr2HzVWjSo51txKv8h","type":"image/jpeg, image/png"}],"categories":[{"id":"people","title":"people"}],"tags":[{"id":"Researcher"},{"id":"Developer"},{"id":"Influencer"}],"media":[{"id":"QmbSWG2FVRaqRkB5ja5sYb9SkmLeNavejdxUm8GaNrSQ6F","name":"Mooly_Sagiv.jpg","caption":"","thumbnail":"QmbSWG2FVRaqRkB5ja5sYb9SkmLeNavejdxUm8GaNrSQ6F","source":"IPFS_IMG"},{"id":"https://www.youtube.com/watch?v=1KR0GnxhNz4","name":"1KR0GnxhNz4","caption":"","thumbnail":"https://www.youtube.com/watch?v=1KR0GnxhNz4","source":"YOUTUBE"},{"id":"https://www.youtube.com/watch?v=R3NP5cA5FVU","name":"R3NP5cA5FVU","caption":"","thumbnail":"https://www.youtube.com/watch?v=R3NP5cA5FVU","source":"YOUTUBE"},{"id":"https://www.youtube.com/watch?v=2fPTV8VLow8","name":"2fPTV8VLow8","caption":"","thumbnail":"https://www.youtube.com/watch?v=2fPTV8VLow8","source":"YOUTUBE"}],"metadata":[{"id":"references","value":"[{\"id\":\"FgmgJZygNQOBq8qP\",\"url\":\"https://www.certora.com/team\",\"description\":\"Source\",\"timestamp\":1779942116012},{\"id\":\"oO3vr8TMH04BC0en\",\"url\":\"https://www.ae-info.org/ae/Member/Sagiv\\\\_Shmuel\",\"description\":\"Academy of Europe\",\"timestamp\":1779942116012},{\"id\":\"iXCJglOBf7JbqtZI\",\"url\":\"https://en-exact-sciences.tau.ac.il/profile/msagiv\",\"description\":\"Tel Aviv University\",\"timestamp\":1779942116012},{\"id\":\"bgyXbu14o9XEmLnd\",\"url\":\"https://www2.sigsoft.org/awards/impactpaper\",\"description\":\"ACM SIGSOFT\",\"timestamp\":1779942116012},{\"id\":\"oJg7rCGrknQ4Pw1p\",\"url\":\"http://www.pl-enthusiast.net/2014/12/02/collaboration-in-pldi-oopsla/\",\"description\":\"PL Enthusiast\",\"timestamp\":1779942116012},{\"id\":\"p3NTtwHsu0ADUPH9\",\"url\":\"https://etaps.org/2023/speakers/mooly-sagiv/\",\"description\":\"ETAPS 2023\",\"timestamp\":1779942116012},{\"id\":\"j6TEO1NDnfGSPhjq\",\"url\":\"https://www.microsoft.com/en-us/research/academic-program/outstanding-collaborator-award/\",\"description\":\"Microsoft Research\",\"timestamp\":1779942116012},{\"id\":\"01P3TYAt3xCDMWN0\",\"url\":\"https://www2.sigsoft.org/awards/impactpaper/\",\"description\":\"SIGSOFT Awards\",\"timestamp\":1779942116012},{\"id\":\"iZ4A6WORLyAM5ndD\",\"url\":\"https://dblp.org/pid/s/SSagiv.html\",\"description\":\"DBLP\",\"timestamp\":1779942116012},{\"id\":\"TJa4Awx719EMWaF9\",\"url\":\"https://2014.splashcon.org/profile/moolysagiv\",\"description\":\"SPLASH 2014\",\"timestamp\":1779942116012},{\"id\":\"r8eOFTRqd7j8Yu2e\",\"description\":\"LinkedIn: Mooly Sagiv\\n\",\"timestamp\":1779942425230,\"url\":\"https://www.linkedin.com/in/mooly-sagiv-87a36010/\"},{\"id\":\"lKwO7E7mMbSjJUor\",\"description\":\"Keynote talk by Mooly Sagiv: Modularity for Accurate Static Analysis of Smart Contracts\\n\",\"timestamp\":1779942961562,\"url\":\"https://www.youtube.com/watch?v=R3NP5cA5FVU\"},{\"id\":\"iF5fYg2yW5QjSpZY\",\"description\":\"🛠 Effective Code Security Tools - Mooly Sagiv\\n\",\"timestamp\":1779943221252,\"url\":\"https://www.youtube.com/watch?v=2fPTV8VLow8\"}]"},{"id":"medium_profile","value":"http://www.pl-enthusiast.net/2014/12/02/collaboration-in-pldi-oopsla/"},{"id":"linkedin_profile","value":"https://www.linkedin.com/in/mooly-sagiv-87a36010/"},{"id":"previous_cid","value":"\"https://ipfs.everipedia.org/ipfs/QmcVGoLdWFSjE7ty4sS5pkHqrAVx35kQ48LLTe3LXi6biE\""},{"id":"commit-message","value":"\"Removed Mooly Sagiv biography and early life section\""},{"id":"previous_cid","value":"QmcVGoLdWFSjE7ty4sS5pkHqrAVx35kQ48LLTe3LXi6biE"}],"events":[{"id":"d84633e4-5773-459e-b409-9ec0dd092fa6","date":"2018-01-01","title":"Co-founded Certora","type":"CREATED","description":"Co-founded Certora, a company focused on scaling formal verification for smart contracts.","link":null,"continent":null,"country":null},{"id":"b1a1f017-f028-4cff-a9b1-ce277ff31533","date":"2016-01-01","title":"Became ACM Fellow","type":"DEFAULT","description":"Recognized as an ACM Fellow for contributions to software engineering and programming languages.","link":null,"continent":null,"country":null},{"id":"fd86c41c-7cbc-498f-be6f-2d4b244342e7","date":"2011-01-01","title":"Received ACM SIGSOFT Impact Paper Award","type":"DEFAULT","description":"Awarded for significant long-term impact on the field of software engineering through seminal publications.","link":null,"continent":null,"country":null},{"id":"660c06af-4650-4dc3-900b-2d0ed59f6132","date":"2005-01-01","title":"Joined Tel Aviv University as Professor","type":"DEFAULT","description":"Became a full Professor at Tel Aviv University, contributing extensively to programming languages research.","link":null,"continent":null,"country":null},{"id":"2fa93bdc-248e-46b4-9ac4-78be5d582463","date":"2002-01-01","title":"Friedrich Wilhelm Bessel Research Award","type":"DEFAULT","description":"Received the Bessel Research Award, acknowledging his influential research methods in formal verification.","link":null,"continent":null,"country":null}],"user":{"id":"0x8af7a19a26d8fbc48defb35aefb15ec8c407f889"},"author":{"id":"0x8af7a19a26d8fbc48defb35aefb15ec8c407f889"},"operator":{"id":"0xd5893989b9952c6568a99F854795AcC5Ae480D56"},"language":"en","version":1,"linkedWikis":{"blockchains":[],"founders":[],"speakers":[]},"recentActivity":"{\"items\":[{\"id\":\"a2fa9ae8-e29f-4f96-9b49-7229023b07df\",\"title\":\"Mooly Sagiv\",\"description\":\"Mooly Sagiv is an influential computer scientist known for his work in formal verification, program analysis, and smart contract security, currently serving as Chief Scientist at Certora.\",\"timestamp\":\"2026-05-28T04:42:57.283Z\",\"category\":\"people\",\"status\":{\"icon\":\"RiGlobalLine\",\"label\":\"Wiki Updated\",\"iconClassName\":\"text-green-500\"},\"user\":{\"name\":\"0x8af7a19a26d8fbc48defb35aefb15ec8c407f889\",\"address\":\"0xd5893989b9952c6568a99F854795AcC5Ae480D56\"},\"button\":{\"label\":\"View Summary\",\"icon\":\"RiFileTextLine\"},\"summarySections\":[{\"title\":\"Content: Lead / Intro paragraph\",\"subtitle\":\"Inserted an inline YouTube video link in the lead paragraph\",\"variant\":\"modified\",\"changeCount\":1,\"changes\":[\"Added inline YouTube link https://youtube.com/watch?v=1KR0GnxhNz4 to the lead paragraph [[1]](#cite-id-FgmgJZygNQOBq8qP) [[11]](#cite-id-r8eOFTRqd7j8Yu2e)\"]},{\"title\":\"Content: Interviews (new section)\",\"subtitle\":\"Added a new 'Interviews' section containing two recorded talks with descriptions and video links\",\"variant\":\"added\",\"changeCount\":2,\"changes\":[\"Added subsection 'Smart Contract Analysis at Fintech Symposium 2019 #01' with YouTube link https://youtube.com/watch?v=R3NP5cA5FVU [[12]](#cite-id-lKwO7E7mMbSjJUor)\",\"Added subsection 'ETHGlobal Workshop on Formal Verification #02' with YouTube link https://youtube.com/watch?v=2fPTV8VLow8 [[13]](#cite-id-iF5fYg2yW5QjSpZY)\"]},{\"title\":\"Media / Videos\",\"subtitle\":\"Added three YouTube media entries to the media/videos array\",\"variant\":\"modified\",\"changeCount\":3,\"changes\":[\"Added video: id=1KR0GnxhNz4, url=https://www.youtube.com/watch?v=1KR0GnxhNz4, source=YOUTUBE\",\"Added video: id=R3NP5cA5FVU, url=https://www.youtube.com/watch?v=R3NP5cA5FVU, source=YOUTUBE\",\"Added video: id=2fPTV8VLow8, url=https://www.youtube.com/watch?v=2fPTV8VLow8, source=YOUTUBE\"]},{\"title\":\"References\",\"subtitle\":\"Appended two YouTube reference entries to the references value array/string\",\"variant\":\"modified\",\"changeCount\":2,\"changes\":[\"Added reference id=lKwO7E7mMbSjJUor, url=https://www.youtube.com/watch?v=R3NP5cA5FVU, description='Keynote talk by Mooly Sagiv: Modularity for Accurate Static Analysis of Smart Contracts'\",\"Added reference id=iF5fYg2yW5QjSpZY, url=https://www.youtube.com/watch?v=2fPTV8VLow8, description='🛠 Effective Code Security Tools - Mooly Sagiv'\"]},{\"title\":\"Metadata: dates\",\"subtitle\":\"Normalized several date strings from 'YYYY-01-01' to 'YYYY-01' format\",\"variant\":\"modified\",\"changeCount\":4,\"changes\":[\"Changed date from 2016-01-01 to 2016-01\",\"Changed date from 2011-01-01 to 2011-01\",\"Changed date from 2005-01-01 to 2005-01\",\"Changed date from 2002-01-01 to 2002-01\"]},{\"title\":\"Metadata: action entries\",\"subtitle\":\"Added 'action' fields with the value 'CREATE'\",\"variant\":\"added\",\"changeCount\":1,\"changes\":[\"Added action 'CREATE' (3 instances)\"]}]}]}"}