Hillel Wayne总结大模型在TLA+建模与验证方面的能力

Hillel Wayne 总结了 AI 在这方面的优势：

• 修复语法
• 解读反例路径
• 减轻负担，比如自动生成 unchanged 变量
• 将自然语言的规约形式化（但是要小心表述的准确性）

劣势：

• 修复模型 spec
• 在没有用户指导的情况下生成 spec（无法生成足够好的非平凡性质）
• 代码生成

但总体来说，其最大价值体现在降低上手难度，可能有利于形式化方法的推广。