Hillel Wayne的论述
Hillel Wayne 总结了 AI 在这方面的优势：
- 修复语法
- 解读反例路径
- 减轻负担，比如自动生成 unchanged 变量
- 将自然语言的规约形式化（但是要小心表述的准确性）
劣势：
- 修复模型 spec
- 在没有用户指导的情况下生成 spec（无法生成足够好的非平凡性质）
- 代码生成
但总体来说，其最大价值体现在降低上手难度，可能有利于形式化方法的推广。
2026-03-12 Hillel Wayne 进行了反思。他注意到之前的想法建立在TLA+专家使用LLM的基础上。对Formal Methods不了解者使用Vibe Coding 生成Spec时，产生的性质并不「有趣」，即会产生平凡的性质。
The AI is only writing “obvious properties”, which fail for reasons like “we missed a guard clause” or “we forgot to update a variable”. It does not seem to be good at writing “subtle” properties that fail due to concurrency, nondeterminism, or bad behavior separated by several steps. Obvious properties are useful for orienting yourself and ensuring the system behaves like you expect, but the actual value in using formal methods comes from the subtle properties.