以太坊基金会（EF）今年预算削减约40%，面临艰难抉择。

以太坊创始人Vitalik Buterin阐述以太坊基金会的新方向：从广泛参与转向聚焦于核心的CROPS（抗审查、开放、隐私、安全）价值观，追求技术上的深刻卓越，如通过AI辅助形式化验证实现无bug以太坊、强共识安全性和最小化中介等。基金会将缩小规模、更加专注，并鼓励外部力量支持ETH资产。

形式化验证（Formal Verification）是通过编写数学证明并由计算机自动验证程序正确性的技术。以太坊联合创始人Vitalik Buterin深入探讨了该技术在区块链、密码学和AI领域的应用，强调其在保证代码安全性、尤其是在智能合约和ZK-EVM等核心组件上的潜力。文章指出，形式化验证并非万能，存在规范遗漏、部分验证等缺陷，但通过AI辅助可大幅提升效率，形成“安全核心+边缘非安全代码”的新安全模型，有望实现防御方优势。

探讨了在重视隐私、安全和主权的前提下，如何构建本地化 AI 智能体环境。作者详细介绍了基于高规范硬件（如 NVIDIA 5090 和 AMD 128GB 统一内存）与 NixOS、llama-server 等软件的配置方案，并提出了通过沙盒隔离、人类确认防火墙及零知识证明 API 来防御 AI 潜在风险的技术路径。

以太坊基金会（EF）发布了新的使命宣言，明确了以太坊作为“避风港技术”的角色，旨在维护技术自我主权、促进去中心化合作，并提供逃生舱口。EF将专注于抗审查、开源、隐私和安全（CROPS），强调在协议层面的去中心化、可验证性、包容性、活性和安全性，以及在应用层面的用户安全和隐私。

本文从更广泛的加密技术视角出发，重新审视了以太坊的根本价值。作者认为以太坊作为“全球共享内存”，其核心用途包括提供数据可用性（作为公共布告板）、作为无需许可的支付系统，以及作为智能合约平台，特别是在抗垃圾邮件、安全存款和数字对象交互方面发挥重要作用。

文章作者认为在当前“混乱时代”，人们对DAO、二次方融资等“民主事物”的热情减退，尽管技术工具更强大。他提出，应将重心从构建硬性决策机制转向开发共识发现工具（如匿名投票、确保契约），以赋予分布式群体发言权，并引导掌握实权的中心化参与者，使其计划获得更广泛支持。

Vitalik Buterin 呼吁以太坊社区在应用层和生态系统接口上采纳更开放、激进的思维，强调在不牺牲审查抵抗、开源、隐私和安全等核心特性的前提下，重新思考各种概念。他鼓励从第一性原理出发，摆脱路径依赖，大胆探索如隐私、L2s 和 AI 影响等新方向，以促进以太坊的强大发展。

Vitalik Buterin 探讨了在日益增长的政府和企业控制下，以太坊的角色。他认为以太坊不应试图解决所有世界问题，而应专注于构建“庇护所技术”，即创建开放、去中心化的数字空间，赋能用户管理风险、构建财富并协同合作，以抵抗外部压力，实现“去极权化”。

文章比较了以太坊的两种最终性机制 Casper FFG 和 Minimmit。作者认为，尽管 Minimmit 的容错率较低（17% 对 33%），但其在对抗审查攻击和客户端错误方面表现更好，因为它倾向于在不确定性下出现“双链竞争”而非错误最终化，这是一种更健康的权衡。