形式方法引导的 Vibe 编码：通过模型驱动工程关闭人工智能生成的安全关键软件的验证循环

Vibe 编码（以最少的审查从自然语言意图接受 LLM 生成的源代码）速度很快，并且可能足以满足低关键性的消费软件。但对于受 DO-178C、IEC 61508 或 ISO 26262 监管的安全关键系统，它不提供认证途径：大语言模型 (LLM) 不提供正式的正确性保证，现有的补救措施针对预训练数据稀缺且工业工具链中缺乏的验证感知语言（Dafny、Verus、Lean）。本文弥补了这一差距。我们提出了 Forge（生成代码的面向形式方法的细化循环）：一种闭环管道，使用已建立的模型驱动工程 (MDE) 基础设施通过形式验证来指导振动编码。通过vibe编码，我们生成Java源代码；然后，我们的管道通过模型转换提取三种不同形式主义中的形式产物，每种形式都由互补验证器检查：演绎验证（Dafny）、通过故障发散细化检查器（FDR4）进行通信顺序过程（CSP）细化，以及在 Isabelle 中使用 Z 机器进行定理证明；每次验证失败都会成为驱动下一次代码生成迭代的结构化纠正提示。 LLM 是草案生成器，MDE 链是鉴别器，开发人员永远不必阅读正式模型。根据经验，我们发现该管道为 LLM 生成的 Java 生成了与标准相关的验证证据——这是迈向认证的一步。