# LLMs are bad at vibing specifications

DevFeed: [LLMs are bad at vibing specifications](<https://devfeed.tech/articles/llms-are-bad-at-vibing-specifications-25489.md>)

Original publisher: [Read original article](<https://buttondown.com/hillelwayne/archive/llms-are-bad-at-vibing-specifications/>)

Author: Hillel Wayne

Published: 2026-03-10T17:12:30Z

Content type: article

Language: en

Sources: [Newsletter feed for Hillel Wayne's Newsletter](<https://devfeed.tech/sources/newsletter-feed-for-hillel-wayne-s-newsletter.md>)

Topics: [Formal methods](<https://devfeed.tech/topics/formal-methods.md>), [Large Language Model](<https://devfeed.tech/topics/llm.md>), [Specifications](<https://devfeed.tech/topics/specifications.md>), [Artificial Intelligence](<https://devfeed.tech/topics/ai.md>)

Tags: [ai](<https://devfeed.tech/tags/ai.md>), [formal-methods](<https://devfeed.tech/tags/formal-methods.md>), [llms](<https://devfeed.tech/tags/llms.md>), [nondeterminism](<https://devfeed.tech/tags/nondeterminism.md>), [specifications](<https://devfeed.tech/tags/specifications.md>), [verification](<https://devfeed.tech/tags/verification.md>)

## AI overview

The article examines AI-generated TLA+ and Alloy specifications through a case study. It argues that these specifications may fail to compile or model-check and often contain tautological or obvious properties rather than subtle properties involving concurrency, nondeterminism, or multi-step bad behavior.

## Source excerpt

No newsletter next week I'll be speaking at InfoQ London. But see below for a book giveaway! LLMs are bad at vibing specifications About a year ago I wrote AI is a gamechanger for TLA+ users, which argued that AI are a "specification force multiplier". That was written from the perspective an TLA+ expert using these tools. A full 4% of Github TLA+ specs now have the word "Claude" somewhere in them. This is interesting to me, because it suggests there was always an interest in formal methods, people just lacked the skills to do it. It's also interesting because it gives me a sense of what happens when beginners use AI to write formal specs. It's not good. As a case study, we'll use this project, which is kind of enough to have vibed out TLA+ and Alloy specs. Looking at a project Starting with the Alloy spec. Here it is in its entirety: module ThreatIntelMesh sig Node {} one sig LocalNode extends Node {} sig Snapshot { owner: one Node, signed: one Bool, signatures: set Signature } sig Signature {} sig Policy { allowUnsignedImport: one Bool } pred canImport[p: Policy, s: Snapshot] { (p.allowUnsignedImport = True) or (s.signed = True) } assert UnsignedImportMustBeDenied { all p: Policy, s: Snapshot | p.allowUnsignedImport = False and s.signed = False implies not canImport[p, s] } assert SignedImportMayBeAccepted { all p: Policy, s: Snapshot | s.signed = True implies canImport[p, s] } check UnsignedImportMustBeDenied for 5 check SignedImportMayBeAccepted for 5 Couple of things to note here: first of all, this doesn't actually compile. It's using the Boolean standard module so needs open util/boolean to function. Second, Boolean is the wrong approach here; you're supposed to use subtyping. sig Snapshot { owner: one Node, - signed: one Bool, signatures: set Signature } + sig SignedSnapshot in Snapshot {} pred canImport[p: Policy, s: Snapshot] { - s.signed = True + s in SignedSnapshot } So we know the person did not actually run these specs. This is somewhat less of a probl