Specs are just markdown with headers (ours included). So what makes one checkable?

on

Disclosure: we build Reqlan, a small language for writing requirements next to code. So the tweet below is partly about us, and I've tried to read it that way rather than defensively.

Earlier this week Tikhon Jelvis posted this:

I was excited to see "spec driven development" become a common talking point...

until I realized that by "spec", most people meant "markdown file with needlessly standardized headers" and not, like, an actual specification

My first reaction was a small wince, because I went and looked at the top level of our own repo. There's a file called spec.md. It is a Markdown file. It has headers (## Overview, ## Key concepts:, ## Syntax). Its second paragraph says, and I promise I didn't plant this:

Ironically these requirements do not use the language, but this should change as the language develops.

So, yes. Point taken, at least partly at our expense.

This post is me trying to take the tweet seriously instead of arguing with it. He's mostly right. The interesting question, I think, is the narrower one hiding underneath: if most "specs" are prose that nothing checks, what would it take to make even part of one checkable? And where does a tool like ours honestly sit on that, which is lower down than I'd like.

Where he's right

Most spec files I've seen in agent workflows (ours included) are prose under headings. Something reads them: the agent, and on a good day a reviewer. Nothing checks them. If the code drifts away from a sentence in the spec, no process anywhere goes red. The sentence just sits there, being wrong in a nicely formatted way.

The standardised headers are the funny part. They're the one bit a machine could check (is there a ## Requirements section? does it have an ID?), and they're also the least interesting bit. You can lint the form of a document all day and learn nothing about whether the system does what the document says.

And to be clear, our .rq files don't escape this by being a different file extension. Here's an idea in Reqlan:

refund_limit {
    A single refund is never more than 50 dollars.
    ...
}

That middle line is prose. Reqlan indexes it and will show it to you (and to an agent) when you ask about the idea, but nothing checks the code against it. If you wrote "never more than 5000 dollars" the tool wouldn't care. I'll come back to what the tool does check, but I don't want to bury this: the sentence part of a Reqlan spec is exactly as uncheckable as the sentence part of a Markdown spec.

What he actually asked for

The replies are where it got interesting. John Crickett asked the obvious question:

So what do you mean by spec?

and Tikhon answered:

Some kind of formal specification you can verify against—it doesn't have to fully specify everything, but it should be pretty thorough in pinning down the properties that matter

The bit I keep re-reading is the middle clause: it doesn't have to fully specify everything. That's not the all-or-nothing position the original tweet sounds like on a first skim. A partial formal spec, thorough on the properties that matter, counts.

Leo Gorodinski added the part I think is the real problem:

EARS is a good way to write requirements, but requirements aren’t a spec.

and, about the requirements-to-plan-to-code chain, that "each step translates natural language into something else, with no guarantee that the meaning is preserved." Tikhon agreed, and then said something I found quite generous:

I am also hoping that we can design formal specification and verification systems that are higher level and easier to understand at a glance, so that translating back to natural language becomes less critical—but that's easier said than done!

Further down, someone going by Joyful Badger asked:

do you have a suggestion for what verification against a spec can look like?

That's the question I want to have a go at. Not the formal-methods answer, which other people can give far better than me, but the boring practical one, for a team whose spec is currently a Markdown file and who isn't about to learn TLA+ this sprint.

A working definition: a line is checkable if something can say no

Here's the decomposition I've landed on, and I don't hold it tightly. For any single line in a spec, ask three things:

  1. What would a violation look like?
  2. What mechanical thing would notice it?
  3. When does that thing run?

If you can't answer the second question, the line is prose. That's fine, lots of good specs are mostly prose, but it means the line is a request, not a check.

Amit Nikhade put the stakes more sharply than I would have:

a real spec says what must never happen, not just what to build. "the agent can refund up to $50, never more" is a spec. three headers and a bullet list is a wish

I'd quibble slightly. Even "never more than $50" is a wish until something can fail on it. But it's a checkable-shaped wish: you can say what a violation looks like (a refund of $50.01), which is question one. Plenty of spec lines can't even get that far ("the checkout should feel fast").

Working from that, here's a rough ladder of what can say no, from cheapest to most expensive. It's a ladder for lines, not documents.

  • Prose. Read by people and agents. Nothing says no.
  • Shape. Required sections, front matter, IDs present. A linter says no when the form is wrong. This is the "needlessly standardized headers" rung. It checks the template, not the claim.
  • Address. The line has a name, and other things point at that name: this test claims to prove it, this function claims to implement it. A checker says no when a name or file points at nothing. It still says nothing about whether the claim is true.
  • Examples. Tests. They say no for the inputs somebody thought to write down: refund(80) should give 50.
  • Properties. Property-based tests. They say no on generated inputs nobody thought of, within whatever the generator covers.
  • Models and proofs. TLA+, Quint, Rocq, Lean. A model checker says no for any reachable state within its bounds that breaks the rule; a proof covers every input, once someone manages to write it. This is the rung closest to what Tikhon means by an actual specification, and I think it's where you'd catch the cousin of the refund rule that's about two refunds racing each other, which no example test of mine would have thought of.

Each rung costs more to write and needs more skill to read. And the useful reframe, for me, is that a spec doesn't sit on one rung. It's a pile of lines on different rungs, and most piles are almost entirely prose. So "is this a real spec?" is maybe the wrong question. "Which of these lines can fail, and on what?" is one you can actually answer, line by line, in an afternoon.

(Tangent: I wrote about Lean in the Reqlan intro post on my other blog, because what excited me about the recent AI-and-Erdős news was that the proofs were checked. I think I was gesturing at the top of this ladder and then went and built something on the third rung. Make of that what you will.)

Where Reqlan actually sits: the address rung, and only that

Here's the honest version, with real output. A tiny repo, everything run on reqlan CLI 0.10.0, 0.14.0 and 0.15.3 with identical output. I scripted the steps so I could re-run them on each version rather than trust my memory of the first run.

refund_limit {
    A single refund is never more than 50 dollars.
    implemented in ["./src/refund.ts"]
    proven by ["./test/refund.test.ts:never refunds more than 50"]
    proven by ["./specs/Refund.tla"]
    @status in-progress
}

refund_audit {
    Every refund records who approved it.
    @status draft
}

src/refund.ts and test/refund.test.ts both start with a pin back to the idea, // rq:["../spec.rq".refund_limit]. Now the uncomfortable part. Here is the whole test:

test("never refunds more than 50", () => {
  expect(1).toBe(1);
});

and here is the whole TLA+ module:

---- MODULE Refund ----
\* placeholder: nobody has written this model yet
====

And:

$ reqlan check
No issues.

That's the address rung in one screen. Every name resolves and every file exists, so check is happy. It doesn't run the test, so it can't know the test asserts 1 == 1. It doesn't run TLC, so it can't know the model is a comment. And refund_audit has nothing pointing at it at all, which check also doesn't mention. You find that by asking the graph:

$ reqlan analyse -i refund_audit
...
### Edges
(none)

So what does fail? Delete the test file:

$ reqlan check
## Issues (2)

./test/refund.test.ts:never refunds more than 50
- spec.rq:4 refund_limit [file_reference]
- spec.rq:4 refund_limit [file_reference]

(Yes, it lists the same line twice. It's on our list to tidy up.) Or rename the idea in spec.rq without touching anything else:

$ reqlan check
## Issues (2)

../spec.rq.refund_limit
- src/refund.ts:1 [comment_link]
- test/refund.test.ts:1 [comment_link]

Both exit 1, so CI goes red. That's it. That's the whole mechanical claim: names and files that point at nothing. I've written tutorials on the rename case and the orphan case if you want to poke at it step by step.

So why bother with the address rung?

Fair question, given everything above. My answer is that it's the joint between the prose and the rungs that can actually say no.

Leo's point was that every translation step loses meaning. An address doesn't preserve meaning either. What it does is make one specific claim explicit and breakable: this test is the evidence for this sentence. Without that, the link between a line of prose and the test that's supposed to back it lives in someone's head, or in a naming convention, or in the agent's context window for about forty minutes. With it, when an agent renames, moves or deletes the evidence, something goes red instead of silently thinning out.

It also changes what a reviewer can ask. Once the link exists, the question "if this sentence were false, would this test fail?" has a definite test to point at. (That's most of what Review the intent, not the diff was about.) In my toy repo the answer is plainly no, and the address is what lets you find that out quickly rather than not at all.

And it gives the expensive rungs somewhere to attach. proven by ["./specs/Refund.tla"] is a perfectly good address for a real model. Reqlan won't run TLC for you; you'd wire that into CI yourself. But the prose line, the model and the code can be joined by name, so when someone does the hard work on the one property that matters, it's visibly hanging off the sentence it's meant to pin down. Fredrick Gabelmann's reply in the same thread is a nice example of the expensive rungs living inside an ordinary spec-driven workflow:

A template isn't a spec until something checks it. I'm exploring formal methods in spec-driven development with a GitHub Spec Kit workflow that lets features opt into TLA+ or Quint modeling after planning. Tasks wait for TLC or Apalache to pass; type checks don't count. It's early, and I haven't needed it for a feature yet.

Opt-in, per feature, gated on the checker actually passing. That seems right to me, and it's compatible with whatever your spec files look like.

What the address rung won't do

Written down plainly, because this is exactly where it would be easy to oversell:

  • It doesn't check the prose. The sentence is as unverified as any Markdown spec.
  • It doesn't judge the test. A test that asserts 1 == 1 passes check, as above. Mutation testing is one way to catch tests that can't fail; it complements this rather than competing with it.
  • It checks files, not test cases. Naming a case (refund.test.ts:never refunds more than 50) doesn't mean the case is checked. Our own test suite confirms the name is stripped before the file-exists check, and in my repo, deleting the test case but keeping the file still gives No issues.
  • It doesn't flag orphans in check. A requirement with nothing pointing at it shows up as Edges (none) in analyse -i, not as a check failure.
  • Markdown <!-- rq: --> pins aren't indexed on 0.10.0, 0.14.0 or 0.15.3, so they can go stale silently. //-style pins in code are checked. That one's a bug on our side, and it's on the list.
  • It doesn't run anything. No tests, no TLC, no Apalache.

Where this leaves me

Tikhon is hoping for formal systems that are higher-level and easier to read at a glance. I'm coming at it from the other end: start from the prose people already write, and make small pieces of it able to fail, starting with the cheapest piece (does the evidence still exist?). I genuinely don't know if those two directions meet in the middle. My hunch, held loosely, is that the useful shape is a spec where most lines are prose, some have addresses, a few have tests, and the two or three that would really hurt have models, and where a tool's job is mainly to show you which is which, honestly, so the prose can't pass itself off as a check.

Which brings me back to that spec.md at the top of our repo. It's still Markdown with headers. I should probably fix that before I write another one of these.

The full thread is here and worth reading past the top. Reqlan docs are at reqlan.com.

Comments

Post a Comment