软件形式化验证，正在迎来规模化的可能

蚂蚁技术研究院把大模型接入Rust形式化验证。KaPilot由多个Agent从文档抽取安全要求、生成验证用例和规约、预检约束，再调用Kani验证并按反馈修复；团队报告完成标准库挑战中的29项，其中16项提交PR。面向星绽OS底层ostd，KVerus提取跨文件依赖，将代码、引理知识与Verus反馈组织为动态知识库，经生成、验证、修复循环推进证明，后续Skills覆盖迁移、规约生成、审查和精简。持续使用中，ostd整体验证进度超过30%，274个API入口完成验证；最近一个月AI辅助PR接近同期合并PR的60%，证明代码膨胀比由1:7.9降至1:6.1。这些是实际项目阶段披露，不能把全部PR都视为AI独立完成；既有论文和开源链接仅作方法背景，形式化验证仍受规约遗漏及安全假设限制。