专题：alloy

本文分析了AI在形式化规范编写中的局限性，指出其生成的代码存在语法错误和逻辑缺陷，无法有效验证系统行为。作者认为，AI在处理复杂属性如并发和非确定性时表现不佳，限制了其在形式化方法中的应用潜力。文章还提到赠书活动的调整，以提高可访问性。