Mooly Sagiv，又名 Shmuel Sagiv，是 Certora 的首席科学家。他共同创立了这家公司，旨在扩大形式化验证的应用，以增强区块链领域智能合约的安全性。^{[1] [11]}

早年生活与教育

Mooly Sagiv 出生于以色列，从小就表现出对数学和计算机科学的天赋。他在以色列理工学院（Technion - Israel Institute of Technology）接受高等教育，并于 1991 年获得计算机科学博士学位。他的博士研究为他未来在软件验证领域的创新奠定了基础。^{[2] [11]}

职业生涯

学术生涯

Mooly Sagiv 的学术生涯始于特拉维夫大学，在那里他从讲师晋升为正教授。他担任特拉维夫大学布拉瓦特尼克计算机科学与人工智能学院的软件系统主席及教授，自 1998 年 4 月起一直担任该职位，这为他后来在数字资产方面的工作奠定了基础。

他的研究重点是程序分析和软件验证。他的研究领域包括静态程序分析、形状分析、抽象解释、逻辑、定理证明、编程语言、形式化方法、数据流分析、程序切片、网络验证和智能合约。他被引用最多的作品是通过三值逻辑解决形状分析问题，并在 TVLA 系统中得以实现。

Sagiv 的出版物探讨了诸如数据流分析、符号执行以及用于分析和验证程序行为的方法等主题。他的学术工作还涉及与定理证明和抽象解释相关的研究。

2006 年 8 月至 2007 年 8 月，Sagiv 在加州大学伯克利分校电气工程与计算机科学系（EECS）担任访问教授。2008 年 8 月至 2010 年 8 月，他在斯坦福大学担任访问研究员。

一项关于编程语言研究社区作者身份和协作的研究将 Sagiv 称为“PLDI 社区的凯文·贝肯（Kevin Bacon）”。

IBM

1990 年 10 月至 1993 年 10 月期间，Sagiv 在以色列海法的 IBM 担任团队负责人。

Certora

2018 年，Sagiv 共同创立了 Certora，这是一家专注于智能合约和基于区块链的软件系统形式化验证的公司。他从 2018 年 11 月至 2025 年 6 月担任首席执行官。

该公司开发了验证工具，旨在分析去中心化金融（DeFi）应用中使用的智能合约和软件系统的行为。

2025 年 6 月，Sagiv 开始担任 Certora 的首席科学家，常驻纽约市大都会区。

他在公司的工作涉及将形式化方法和软件验证技术应用于区块链相关系统和智能合约。

协作与专业活动

Sagiv 参与了与编程语言和软件工程相关的合作研究项目。他的工作包括涉及程序分析和软件验证的协作。

他还参加了与计算机科学和软件工程相关的会议和研讨会，包括欧洲编程研讨会（ESOP）和国际软件工程会议。

奖项与认可

Sagiv 于 1989 年获得沃尔夫基金会奖学金，并于 1993 年获得 IBM 杰出技术成就奖。2000 年至 2005 年间，他获得了 IBM 教师奖。

2002 年，他获得了弗里德里希·威廉·贝塞尔研究奖（Friedrich Wilhelm Bessel Research Award）。

2011 年，Sagiv 与 Thomas Reps、Susan Horowitz 和 Genevieve Rosay 共同获得了 ACM SIGSOFT 回顾性影响力论文奖。

2016 年，他获得了微软杰出合作伙伴奖，并被评为 ACM 会士。

他在软件工程、程序分析和形式化方法方面的工作通过学术奖项、研究协作以及在学术界和工业界的职位得到了认可。^{[1] [2] [3] [4] [5] [6] [7] [8] [9] [10] [11]}

采访

2019 年金融科技研讨会上的智能合约分析 #01

2019 年 7 月 15 日，Mooly Sagiv 在由 YouTube 频道“Datalogisk Institut - Københavns Universitet”主办的 2019 年金融科技研讨会上发表了题为“智能合约精确静态分析的模块化”的主旨演讲。

在演讲中，Sagiv 讨论了智能合约静态分析的方法，重点是旨在识别软件漏洞并在部署前验证特定程序属性的技术。他指出，由于分析精度的限制，一些现有的工业分析工具可能会产生误报或无法检测到某些错误。

Sagiv 描述了一种被称为精确静态分析（ASA）的方法，该方法在以太坊虚拟机（EVM）字节码而非源代码上运行。根据演示，这种方法允许在源代码文件不可用时也能对合约进行分析。

演讲还讨论了模块化验证方法，旨在根据外部合约的预期行为和系统要求来评估合约。其他主题包括形式化规范、重入漏洞、金融逻辑条件以及在智能合约开发工作流程中使用自动化验证程序。^[12]

ETHGlobal 形式化验证研讨会 #02

2022 年 10 月 18 日，Mooly Sagiv 参加了 ETHGlobal YouTube 频道主办的题为“有效的代码安全工具”的研讨会。在会议期间，他讨论了与智能合约安全分析相关的挑战，包括现有审计和静态分析工具中的误报和未检测到的漏洞。

在演示中，Sagiv 将形式化验证描述为一种将智能合约代码与旨在定义预期系统行为的数学规范相结合的方法。他解释说，Certora 的验证框架分析编译后的 EVM 字节码，以评估在执行过程中是否保持了预定义的条件和不变性。

研讨会包括了与去中心化金融（DeFi）协议和自动做市商相关的示例。Sagiv 表示，基于规范的验证可用于识别涉及偿付能力条件、不变性违规和边缘情况执行场景的情况。他还将形式化验证描述为一个可以与人工审计、模糊测试和其他安全审查方法一起使用的过程。

会议进一步讨论了形式化规范在软件开发工作流程中的作用。Sagiv 指出，当验证过程贯穿整个开发过程，而不是仅在后期审计期间应用时，验证过程会更有效。^[13]