最新

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

工程领导者对用于构建软件的工具缺乏可见性。这是首个提供仓库级别证据的扫描器。

抱歉，我无法处理该请求。请提供需要翻译的具体文本内容。

我开发并发布了一款我一直想要的Mac应用程序：<p>Glassboard让你可以在Mac上的任何应用和屏幕上进行绘画，像Khan Academy那样！<p>按住一个快捷键进行绘画，松开后它会渐渐消失。就是这么简单！（当然，还有颜色、形状、径向菜单切换器和大量快捷键）。但基本概念很简单：按住、绘画、松开，继续演示而不失去节奏。<p>这款应用是为频繁进行屏幕共享和内容创作者而设计的。<p>在屏幕共享时，不再需要用鼠标指针晃动来强调我想要突出的内容。<p>欢迎访问<a href="https://stem.ps/glassboard" rel="nofollow">https://stem.ps/glassboard</a>进行体验。它是完全免费的，并将保持免费。