一周热榜

<a href="https://developers.googleblog.com/en/announcing-the-agentic-resource-discovery-specification/" rel="nofollow">https://developers.googleblog.com/en/announcing-the-agentic-...</a>

在 Cajal (YC W26)，我们很高兴推出 Talos（[https://github.com/cajal-technologies/talos](https://github.com/cajal-technologies/talos)），这是一个用于在 Lean 中对 WebAssembly 模块进行形式化验证的开源框架。 人工智能现在正在编写大量用于生产的代码。随着代码生成成本的降低，验证成为了瓶颈。我们相信，未来每一段软件都将附带一个数学证明，证明它实现了作者的意图——从而消除许多类型的漏洞。Talos 是实现这一目标的基础之一。 Talos 提供了一个针对二进制级别推理优化的 Wasm 解释器，以及一个用于证明程序属性的最弱前置条件演算层。由于我们直接对 WebAssembly 进行推理，因此任何具有 Wasm 后端的语言都在支持范围内：Rust、C++、Go、C、Swift、Kotlin、Zig、C# 等等。 为了实现这一点，我们使用了 Lean：一种编程语言和定理证明器，它允许您在一个系统中同时编写软件并对其进行数学证明。这使得 Talos 既可以作为可执行解释器，也可以作为 Lean 进行推理的形式化对象。Lean 还集成了现代人工智能证明工具，通过证明搜索和直接评估自动处理目标。 要查看 Talos 的实际应用，请查看对流行的 Rust crate num-integer 中实现的 Stein 的 GCD 算法的证明：[https://github.com/cajal-technologies/talos/blob/main/programs/lean/Project/NumInteger/Spec.lean#L562-L588](https://github.com/cajal-technologies/talos/blob/main/programs/lean/Project/NumInteger/Spec.lean#L562-L588)。 我们的路线图： - 通过首先通过官方 W3C 测试套件，然后对 SpecTec（形式化 Wasm 规范）进行验证，实现完整的 Wasm 覆盖。 - 任意 crate 验证——任何编译到 Wasm 的 Rust crate 都应在支持范围内。 - 构建我们的证明库 codelib，以使验证日益复杂的程序变得可行。 我们非常希望听到社区对 Talos 的反馈以及对当前形式化验证状态的评论。也欢迎贡献！

大约一年前我在这里发布了我的作品集（<a href="https:&#x2F;&#x2F;news.ycombinator.com&#x2F;item?id=45154609">https:&#x2F;&#x2F;news.ycombinator.com&#x2F;item?id=45154609</a>），虽然反响很大，但褒贬不一！这次可能也会类似，但无论你对这个概念有什么看法，我认为我成功地创造了一个互联网上最怀旧的角落，尤其是加上最新的内容。 关于这是否是一种比标准、快速、简单的作品集更有效的吸引注意力的方式，这可能永远会有争议，但我坚信，这对于双方来说都更有趣，而且是毋庸置疑的。

你在忙什么？有什么新想法吗？