LLMs are bad at vibing specifications

作者通过分析AI生成的TLA+和Alloy规范案例，指出大型语言模型在编写形式化规范时存在严重问题：它们倾向于生成"显而易见"但无实际验证价值的属性，而无法捕捉并发、非确定性或多步骤交互中的微妙错误。即使AI降低了形式化方法的入门门槛，但若用户本身缺乏专业知识，仍难以获得真正有用的验证结果。