Show HN: Salt – a systems language with Z3 theorem proving in the compiler21 days agohttps://salt-lang.devSalt 通过 Z3 验证的合约在编译时提供经过验证的安全性，无需运行时开销。它使用区域分配而非垃圾回收或借用检查器，确保内存安全并防止泄漏。在各类基准测试中，包括机器学习推理、内核、网络和渲染，Salt 的性能与 clang -O3 相当。该语言具备管道操作符用于链式调用、可选的错误链式处理，以及无需分配的类型安全格式化 f-strings。Salt 的包管理器 sp 提供依赖验证、内容寻址缓存和单仓库支持，以实现快速可靠的构建。
Leanstral 1.5: Proof Abundance for All19 days agohttps://mistral.ai/news/leanstral-1-5/Leanstral 1.5 是一款采用 Apache-2.0 开源许可的免费模型，拥有 60 亿激活参数，在形式验证方面提供了显著的性能提升。它在多个基准测试中取得了最先进的成果：在 miniF2F 上达到 100%，在 PutnamBench 上达到 587/672，在 FATE-H 上达到 87%，在 FATE-X 上达到 34%。该模型经历了一个三阶段的训练过程：中期训练、监督微调以及使用 CISPO 配合多轮和代码代理环境进行的强化学习。它在 PutnamBench 上展示了强大的测试时扩展能力，随着计算预算（token 数量）的增加能解决更多问题，从 5 万 token 下的 44 个问题，到 400 万 token 下的 587 个问题。Leanstral 1.5 在代码验证方面表现出色，证明了 AVL 树的时间复杂度，并在测试的 57 个代码库中发现了 5 个之前未知的错误。该模型已完全开源，可通过 Hugging Face 和免费 API 获取，并建议使用 Mistral Vibe 和 Lean LSP MCP 进行环境配置。
Lean Software Scaling Laws17 days agohttps://gwern.net/lean-scaling提议测量编码大型语言模型（LLM）困惑度如何随代码库上下文规模扩展，使用 Lean 作为形式化语言的测试案例。旨在通过编程语言估计“可预测性”的缩放定律，转化为软件安全性和可靠性的改进。Lean 可能具有更差的基线性能但更优的缩放指数，表明对程序正确性和网络安全具有长期益处。方法论涉及通过冻结的 LLM 进行实证测量、语料库构建、损失测量和每种语言的缩放定律拟合。预测：像 Python 这样的“弱”语言在小规模下表现出色但缩放指数更差，而像 Lean 这样的“强”语言在大规模下实现反超。需要控制程序员和领域差异的偏差；考虑了上下文学习及失败模式（如生态系统成熟度的影响）。
ESBMC-Arduino: Closing the Deployment Gap for Formal Verification8 days agohttps://arxiv.org/abs/2607.08550本文介绍了ESBMC-Arduino，以弥合运行在微控制器（如Arduino）上的开源硬件PLC形式化验证中的部署差距。文章强调，缺乏硬件输入模型的朴素宽度感知验证会导致误报，如在123个真实程序中出现了44%的误报率。提出了一种基于硬件精准的验证方法，该方法利用声明式HAL描述符和健全的降低策略，以目标宽度解释算术运算，并将输入约束在硬件可实现范围内。该方法以ArduinoTool形式实现，在保持鲁棒性证明的同时消除了所有误报，并能通过可实现的反例检测罕见的宽度相关缺陷。
Formal verification might solve AI's review bottleneck19 hours agohttps://georgwiese.github.io/posts/formal-verification-ai/一种新的软件工程范式结合了形式验证与人工智能：人类用形式语言（如Lean）定义需求，AI编写代码并附带机器可验证的正确性证明，从而消除对生成代码的人工审查。仅靠AI面临审查瓶颈——它能以近乎零成本编写代码，但审查所有代码成为新瓶颈；形式验证通过自动证明正确性消除了这一瓶颈，并附带提升可信度。该框架涉及人类定义硬约束（形式规范）和优化目标（基准测试），AI代理编写代码和证明；由于约束被自动证明、目标被自动测量，人类投入极少。与机器学习的类比包括过拟合和规范钻空子等风险，代理可能利用规范中的缺陷；需要正则化、精心设计指标等工具来管理这些风险。一个Hello World示例（第k小元素）展示了该方法：Lean定义捕获正确性，代理填充实现和证明，基准测试优化运行时；代理从排序改进为快速选择。在powdr（zkVM的自动预编译）的案例研究中取得成功：500行Lean规范、用于优化的基准测试，100%由AI生成代码和证明且无需人工审查；电路规模缩减与先前实现持平，运行时显著提升。若编写规范比维护代码成本更低，该方法可能推广，可重用规范库或有助益；通过FFI集成可实现渐进式采用，可能将软件工程重心从代码转向需求。