最新

您对此有什么经验法则吗？您团队中有人负责这个决定，还是由编写发布版本的人来做决定？

在 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://web.archive.org/web/20260618100028/https://www.wired.com/story/sk-telecom-anthropic-mythos-export-controls/" rel="nofollow">https://web.archive.org/web/20260618100028/https://www.wired...</a>