Argot : 2025 年以太坊基础设施更新路线图

编者注： Argot 是由以太坊基金会的员工重组成的一个非营利研究与开发小组，专注于维护与以太坊相关的自由和独立软件。专门从事编译器工程、验证和编程语言理论。

在 Argot，我们正在为以太坊应用构建关键基础设施。我们的使命是开发和维护核心编程语言和工具，以确保应用开发的安全性和弹性。

2025 年已经成为具有里程碑意义的一年：我们注册成为一家瑞士非营利协会，获得了初始资金，并重新发布了我们的网站。在建立了管理基础之后，我们现在可以优先考虑我们最擅长的事情——构建基础设施——并投入更多精力来确保可持续的长期资金。

这篇博文涵盖了六个关键项目，涉及编程语言、开发者工具和形式化验证。在下文中，你将了解到 2025 年剩余时间里将会发生什么。

编程语言

Solidity

Github | 社交媒体 | 网站

在以太坊的主要智能合约语言庆祝其成立 10 周年之际，Solidity 继续在创新与稳定之间取得平衡，因为数十亿美元的智能合约都依赖于它。该项目目前正在开发 Core Solidity，这是该语言的下一个迭代版本，最终将成为 Solidity 1.0。它将实现快速的功能开发，同时保持精简、稳定的基础。我们的目标是使合约正确性的验证更容易，并成为一种更常见的实践。

以下你将看到 Solidity 的 2025 年路线图，尽管社区的意见将影响下一步的发展方向。随着 Solidity 迎来 10 周年，并且我们在组织上进行转型，我们正在重新评估多年来积累的功能请求以及我们的总体目标。虽然我们的重点仍然是语言和代码生成管道的稳定，但我们正在探索针对当前痛点的短期解决方案。我们很快将发布一份“路线图愿望清单”，其中涵盖这些功能、它们的可行性和权衡。

近期里程碑

• 发布了 v0.8.30。
• 添加了对自定义存储布局的支持。
• 引入了初始的 ethdebug 支持。
• 与 Ipsilon 团队合作，实现了实验性的 EOF 支持。
• 实验性的 SSA CFG IR 管道的初步工作。该管道使用静态单赋值形式的 Yul 代码的控制流图，旨在解决 Yul 优化器和 Yul->EVM 转换的性能问题。
• 与马德里大学的研究人员合作启动了 Project GreY，旨在提高 Yul->EVM 转换的效率。
• 发布了第五次年度 Solidity 开发者调查的结果。

团队说明：

• 随着 Solidity 加入 Argot 成为以太坊核心基础设施的新家，2025 年的大部分时间都致力于为 Argot 的成功发布做准备。
• 前团队负责人 Daniel Kirchner 目前正在休假。有关他未来参与情况的更新将在稍后发布。
• 与 Argot 的非层级方法保持一致，每位经验丰富的团队成员都以相当大的自主性运作。Kamil Śliwak，前 Solidity 联合负责人，在此过渡期间担任项目负责人。

2025 年路线图

Q3

• 基于 SSA-CFG 的 Yul 后端，具有内存溢出功能。
• 使用 hevm 对 SSA CFG 后端进行差异模糊测试。
• 在 Yul 中切换到数值 AST 节点 ID，以获得更好的优化器性能并防止重复出现的字节码可重现性问题。
• 支持存储布局说明符中的常量和 erc7702() 辅助函数。
• ARM 架构的官方 Linux 二进制文件。
• 元数据改进和源代码验证的额外输出。
• 为了迎接下一个重大版本 (0.9.0) 而弃用功能。

Q4

• 可以支持 ERC20 代币功能的 Core Solidity 原型。
• SSA CFG 管道的优化器通道的实现。
• 对 ethdebug 的部分支持。
• Solidity 级别的内存优化的设计工作。
• 分析后对错误进行合理的报告。
• 编译器为 Fusaka 网络升级做好准备。

Fe & Sonatina

Fe Github & Sonatina Github | 社交媒体 | 网站 | 社区

Fe 代表了 Argot 在语言方面的实验性、前瞻性工作，它将类似 Rust 的语法与高级类型系统功能相结合。它的后端 Sonatina 专注于激进的优化，以生成高性能、可验证的 EVM 字节码。它们共同旨在为开发者提供一个富有表现力、高性能且可验证的下一代工具链。

Fe 的主要目标是完善作为 v2 代码生成先决条件的基础高级语言功能，同时提供全面的 CLI 和语言服务器工具。与此同时，Sonatina 的重点是发布一个完全集成到 Fe 工具链中的生产就绪 v1 后端，同时推进关于 VSDG + 分离逻辑 IR (v2) 的基础研发，该 IR 可以扩展到 EVM 之外，并能够对合约状态和副作用进行精确推理。

近期里程碑

• 完成 Fe v2 解析器/分析重写。
• 内置核心库，具有改进的类型/路径解析改进。
• 增强的模式匹配诊断。
• 具有 TCP 支持的异步语言服务器重写。
• 扩展的编辑器支持（VSCode、Zed、Neovim）。

2025 年路线图

Q3 (Fe)

• 启用 trait 关联的类型定义和类型投影。
• 支持从本地路径和远程 git URL 加载库。

Q4 (Fe)

• 语言服务器改进（代码完成、重构功能）。
• 核心/标准库，带有基本的数据结构和特定于 EVM 的实用程序。
• 全面的 v2 文档。
• 具有草案语法和语义的 Actor/消息传递模型。
• 用于副作用管理和基于能力的安全性代数效应原型。

Q3–Q4 (Sonatina)

• 完成 v1 代码生成阶段，并具有完整的 CI 覆盖。
• 完成 v1 的 e-graph 优化，包括集成等式饱和引擎，以在降低之前执行常见的子表达式消除、代数简化和窥孔重写。
• 将 v1 合并到带有 --backend Sonatina 标志的 Fe 编译器中，发布候选版本，并收集早期采用者的反馈。
• 推进基于 VSDG 分离逻辑的 v2 IR，以增强效应/能力跟踪和跨目标可行性。

开发者工具

Sourcify

Github | 社交媒体 | 网站

Sourcify 已经改变了智能合约验证，从 2024 年 8 月的 510 万个经过验证的合约增长到 2025 年 8 月的 850 万个。该项目旨在发挥协调者和构建者的作用，以创建一个开放、去中心化和动态的智能合约验证生态系统，该生态系统由开源工具、可访问的数据集和共享标准提供支持。其使命是在维护以太坊透明性和无需信任的核心价值观的同时，加强 EVM 工具的格局。

近期里程碑

• 推出了 API v2，具有基于票证的路由、更清晰的端点、std-JSON 支持、更丰富的错误和一个新的 DB，该 DB 表面了完整的验证诊断。现在支持 Vyper。
• 使用模块化设计重构了 lib-sourcify，将云使用量减少了 >50%。
• 部署了统一的 Remix 插件作为第一个“随处验证”集成，为 Foundry 和 Hardhat 铺平了道路。
• 与 Sourcify–Blockscout–Routescan 联合注册表建立了 Verifier Alliance，用于交叉检查合约数据。
• 发布了简化的验证应用程序 (verify.sourcify.dev) 和存储库查看器 (repo.sourcify.dev)。
• 编写了 EIP-7834（EOF 的元数据部分），以简化未来的验证。不幸的是，EOF 未发布，并强制执行当前解决方法。

2025 年路线图

Q3

• 4bytes DB：全面的 4 字节签名 DB 和精心设计的 API。
• 用于社区合约查询的公共可查询 DB 实例。
• 通过链合作伙伴关系扩大经过验证的合约覆盖范围。

Q4

• 未经验证合约的字节码相似性搜索。
• 通过会议、聚会等方式提高在线和现实生活中的知名度。

在项目博客上查找有关 Sourcify 的使命和目标的更详细的 文章。

Ethdebug

Github | 社交媒体 | 网站

ethdebug 格式是一种用于智能合约的调试数据格式标准，使编译器能够向开发工具提供丰富的调试信息。在建立初始设计并达成社区共识后，ethdebug 现在正在过渡到实施阶段，早期采用者开始集成该格式。

近期里程碑

• 初始的实验性 ethdebug 支持已在 Solidity 0.8.29 中实现（2025 年 3 月）。
• 发布了指针解引用的参考实现 (@ethdebug/pointers)。
• 与 Solidity、Tenderly 和其他团队建立了定期的双周工作组会议。
• 在 Devcon SEA 上介绍了项目概述和状态。

2025 年路线图

Q3-Q4

• 使用演示完整格式用法的玩具编译器扩展参考实现，并将调试器端参考扩展到指针之外，以包括程序模式支持。
• 推动编译器集成，使其超出 Solidity 的初始实验性支持。
• 建立 Fe 集成路线图并启动 Vyper 团队讨论。

Q4

• 完成 v1 模式规范：
  • 最终确定函数调用语义模式。
  • 解决指针模板变量重命名限制。
  • 扩展类型模式以支持通用类型规范。
• 通过 Tenderly 和 Simbolik (RV) 合作推动调试器生态系统采用。
• 记录最佳实践和集成指南。

形式化验证

Act

Github | 文档

Act 是我们用于 EVM 智能合约的形式化验证和文档工具。当前用 Haskell 编写的实现已成功用于证明标准合约（如 ERC20 代币和自动做市商 (AMM)）的端到端正确性。展望未来，重点是加强其数学基础、扩展其表达能力以及扩大在开发者和研究社区中的采用。

近期里程碑

• 支持将地址强制转换为合约类型。
• ERC20 的端到端验证。
• 在语义定义方面的进展。

2025 年路线图

Q3-4

• 引入博弈论推理，并通过 CheckMate 工具集成进行验证后端。
• 使用精确的语义定义来形式化 Act 的数学基础。

Q4

• 实际案例研究：Uniswap v2 和 MakerDAO 合约验证。
• 通过支持其他数据类型（例如数组、结构）和未知代码推理来增强可扩展性和表达能力。
• 发布基础研究论文以降低采用障碍。
• 从基本用法到高级扩展的全面文档套件。
• 官方 v1.0 版本发布。

Hevm

Github | 网站

Hevm 仍然是以太坊智能合约的符号执行和测试的基石工具。通过发现边缘情况并实现严格的分析，它在确保合约安全方面发挥着重要作用。下一阶段的工作旨在扩大其用户群、突出实际影响并扩展高级分析功能。

近期里程碑

• 通过改进的文档和新手入门来改进网站。
• 发布了 hevm v0.55.1，其中包含可用性、覆盖率和速度改进。
• 添加了更完整的 Foundry 作弊码支持。
• 将符号执行集成到 Echidna 和 Solidity 模糊测试管道中取得了进展。
• 更新了 Nix 和 Forge 依赖项。

2025 年路线图

Q3-4

• 通过教程、研讨会和会议演示进行教育和推广。
• 通过具有在线界面的 WebAssembly 构建实现零安装访问，并可能通过 Remix 集成插件实现即时、基于浏览器的使用。
• 具有版本控制的、记录在案的接口的稳定集成 API。

Q4

• 通过分析和重构周期来增强开发者体验。

• 通过使用 hevm 检测和确认至少一个生产级漏洞来展示实际影响。

• 高级分析功能，可以选择将外部调用限制为预加载合约和扩大搜索范围，以及自动重播和验证所有生成的反例以消除误报。

• 通过 Echidna 集成 Concolic 执行，结合模糊测试和符号方法以实现更深层次的路径发现。

• • *

通过我们的半年期路线图更新和各个项目沟通，随时了解 Argot 的进展。

在 X、Bluesky 或 farcaster 上关注我们。

• 原文链接： argot.org/blog/2025-road...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～