AutoProver 推出:面向每位开发者的智能形式化验证

Certora 发布于 2026-07-16 阅读 44

Certora 推出 AutoProver,这是一个基于 AI 的形式化验证系统,能够读取代码和文档,自动生成规范、测试和形式化证明。它解决了逻辑错误难以捕获、AI 生成代码缺乏保证以及形式化验证难以扩展的问题。通过 Agent 流水线,从理解代码、生成规范、生成测试和证明,到执行调查和迭代,全部自动化。结果输出结构化的漏洞报告和验证资产,可集成到开发工作流中。目前支持 Solidity,Rust 即将支持。

形式化验证是唯一能够证明整个类别的漏洞不可能发生的方法。然而,对大多数开发者来说,它一直难以触及,因为这需要专业知识和大量的人工投入。

过去七年,Certora 通过人工审计和形式化验证帮助保护了 DeFi 中一些最关键协议的安全。今天,我们将这些经验带入 AutoProver:一个能读取你的代码和文档,生成形式化规范与测试,并使用最先进的形式化方法对你的软件进行形式化验证的系统。

结果是代码更安全、更易于维护,且每个开发者都能使用形式化验证。

AutoProver Beta 版现适用于 Solidity,Rust 即将推出。它与现有的大语言模型(LLM)集成,易于纳入开发工作流。

问题:交付速度已超越交付信心

如今开发速度比以往任何时候都快,但信心却未能同步跟上。主要有三方面障碍。

  • 逻辑漏洞难以发现。 最棘手的错误是逻辑错误,而非语法错误。它们能通过编译和测试,往往还能逃过代码审查。然后几周或几个月后,正确的交易序列才会暴露它们。人工代码审查能发现部分此类漏洞,但速度慢、成本高且无法扩展。
  • AI 生成的代码缺乏保证。 模型不断改进,但产生的结果具有非确定性,并且没有精确的意图概念。AI 可以非常出色地生成可工作代码,但它无法理解这些行为是否符合你的意图。它还可能引入细微的回归问题,在审查时看起来完全合理。
  • 形式化验证无法规模化。 形式化验证很困难,因为编写好的规范需要经验。大多数团队无法让形式化方法专家与每个开发者并肩工作。

解决方案:从意图到证明的智能体流水线

AutoProver 集成了基于多年形式化验证研究和工程构建的专门 AI 智能体。工作流程非常简单:

1. 理解你的代码

你让 AutoProver 指向你的仓库,它便开始工作。它首先处理已有的代码,利用文档和设计文档来构建对系统更丰富的理解。

2. 生成形式化规范

它将这种理解转化为覆盖单个组件以及跨系统交互的形式化属性。这些规范描述了预期行为,独立于当前实现。

3. 生成测试和证明

根据这些属性,AutoProver 生成测试(目前基于 Foundry)、Certora Prover 的 CVL 规则,以及证明正确性所需的支持性验证代码。

Image

4. 执行与调查

专门的智能体运行生成的测试和证明,对失败进行分诊,并排查验证问题。另一个智能体寻找未被明确指定的漏洞,利用了 Certora 多年验证工作中积累的常见漏洞模式。

5. 审查结果。 你会收到一份结构化报告,包含三部分:代码漏洞、设计漏洞,以及每个属性的完整状态及其测试、规则和结果。

6. 迭代。 审查发现,提供反馈,并重新运行。AutoProver 会随着时间从你的输入中学习。当你准备好时,你可以提交一个包含生成验证资产的 PR,并随着代码演进持续改进你的验证套件。

Image

超越模式匹配

大多数 AI 代码审查工具基于模式匹配标记潜在问题。AutoProver 采用根本不同的方法:它生成形式化规范,并使用最先进的形式化验证方法数学证明你代码的属性。

与对话式 AI 工具不同,AutoProver 生成验证资产,并成为你开发工作流的一部分。 它产生的测试、规范和验证规则可以与应用程序一起审查、版本化并维护,逐步发展成长期的验证套件。

"我研究形式化方法已经超过四十年,编写规范始终是瓶颈," Certora 联合创始人 Mooly Sagiv 表示,"大语言模型正在改变软件的编写方式,但它们并没有解决正确性问题。甚至可以说,它们让这个问题变得更加重要。AI 现在可以帮助解决形式化验证中最困难的部分之一,使其对更多开发者变得实用和可及。"

像运行编译器一样简单

运行 AutoProver 应该像运行编译器或任何其他开发工具一样自然。AI 已经改变了我们编写软件的速度。AutoProver 旨在帮助我们以同样的速度信任这些软件。

立即开始

AutoProver Beta 版现适用于 Solidity,Rust 即将推出。

开始使用: https://app.certora.com/

  • 原文链接: certora.com/blog/autopro...
  • 登链社区 AI 助手,为大家转译优秀英文文章,如有翻译不通的地方,还请包涵~

相关文章

0 条评论