#形式化验证
共 12 篇相关文章
Claude形式化验证：为123个开源库证明无崩溃
Anthropic用Claude对123个OSS-Fuzz开源库进行形式化验证，证明无崩溃性质。本文解析证明覆盖范围、适用边界，以及值得借鉴的fuzz target编写习惯。
大模型如何让形式化软件验证走向大规模落地
Hacker News 讨论指出，大型语言模型正在降低形式化软件验证的成本门槛。本文分析 LLM 在规格生成、证明脚本草拟、不变式发现等环节的切入点，并强调信任边界不可模糊：模型负责提出，证明器负责裁决。
AI发现新共识协议A-greement，分布式系统研究被改写？
AI智能体框架AI-greement自主发现新共识协议A-greement，在geo-replicated状态机复制中延迟降低高达33.3%，并利用Lean形式化验证发现现有协议漏洞。研究强调人类专家仍不可或缺，共识研究进入人机协作新阶段。
Maestro：全局协调破解Lean证明失败难题
Maestro是面向Lean的形式化证明框架，通过全局协调器区分证明失败原因并重新规划，在PutnamBench、Lean-IMO-Bench等基准上超越现有证明器与原生编码代理。
用证据系统驾驭AI代理：形式化验证加密代码的治理实践
Reddit开发者分享用"证据系统"治理AI代理编写形式化验证加密代码的实践：通过规格映射、验证器输出、反例记录与不确定性声明，把凭直觉的协作转为可审计的治理机制，并讨论人类审查角色的转变与证据系统自身的风险。
Lean正式集成已验证内核，可靠性与性能双突破
Lean 定理证明器正式发布经过形式化验证的内核，提升证明可信度并强化可信计算基。本文分析其对生态的影响、性能权衡及社区反应。
Lean编程入门：将需求转变为机器验证的定理
从有界计数器到库存状态不变式，本文演示如何用Lean定理证明器把程序需求写成数学规约并完成机器检查证明，同时说明形式化验证能保证什么、不能保证什么，以及如何把规约集成进CI流程。
验证与迁移：精确信息前沿及调用代价
论文《Verification with Transfer》用列表率失真函数精确刻画验证迁移的信息前沿与调用代价，给出精确/噪声验证器下的分岔结论、F₂ 线性源库闭式解，并在 Lean 4 中机器验证。
OpenAI的Navier-Stokes证明与Lean代码不一致：形式化验证的隐忧
OpenAI的Navier-Stokes方程证明与其Lean形式化代码存在不一致，arXiv论文指出mis-translation问题，另有工程师用NanoLean在17秒内验证通过。本文解析二者为何殊途同归：形式化验证通过不等于原始证明正确。
Lean之父Leo de Moura深度访谈：当AI开始攻击数学证明内核
Lean之父Leo de Moura深度访谈：AI利用两个内核漏洞伪造Collatz猜想证明，同时又写出比Rust更快的已证明Zlib代码。探讨形式化验证如何应对AI的奖励黑客、信任最小化策略，以及人类在数学与软件工程中不可替代的角色。
AI生成数学证明该如何负责任地发布？
AI已能生成数学证明，但如何负责任地发布这些成果成为难题。本文探讨AI数学成果的验证挑战、形式化证明工具的作用以及学术界应建立的透明披露规范。
Verus：用形式化验证打造可证明正确的Rust代码
Verus是面向Rust的程序验证器，通过对照数学化功能规范自动检查代码，实现可证明正确的Rust程序，为加密、内核等高安全场景提供数学级正确性保证。本文解析其工作原理与工程价值。