Who checks the Checker?

TL;DR

Just for fun, I ran Prover’s Requirement Quality Checker on three requirements that an AI (Gemini 3.1 Pro) extracted from my short story The Time Lock, with the story passage as context. All three failed, and each verdict came back in 15 to 30 seconds.
The diagnoses were good. Across 15 criterion checks, 1 passed, 5 warned and 9 failed; Verifiable failed every time. It found a real syntactic ambiguity (“confirming test data”) and used the story to connect “allied forces” with the “Federation forces” of the text.
Each suggested rewrite has the same shape, the event-driven pattern When ⟨trigger⟩, the ⟨system⟩ shall ⟨response⟩, with unknowns left as ⟨placeholders⟩.
The rewrites don’t always apply their own critique. Two of them keep a phrase the checker had just flagged (“critical research findings”, “receive and store”), and one introduces an actor (“the operator”) that appears nowhere in the story.
Limits: three requirements, one run each, no known-good requirement as a control, and a rate limit of three checks. Nothing here is a measurement of accuracy.

Wait! Why are we doing this?

I’m reading up on formal verification of AI-generated output, with an agent in the loop. Two weeks ago I came across Prover, a Swedish/French company that verifies railway signalling software, and I’ve been learning about the field since. Their Labs page has a few AI tools you can try in the browser. One of them checks the quality of a single requirement. I was curious: what does a machine count as an ambiguous sentence?

…and what exactly are we looking for?

In terms for verification, ambiguitiy is like a frightning ghost. But ambiguity itself is somewhat ambiguous. What exactly is the requirement quality checker looking for? Well, okay, I don’t work at Prover, but from what I understand the checker grades a requirement on five criteria: unambiguous, verifiable, understandable, singular and complete. In linguistic terms, each one is about a different layer of the sentence:

Criterion	A requirement has it when…	The linguistic question
Unambiguous	its form and content allow only one reasonable interpretation in context	Is there lexical, syntactic, semantic or referential ambiguity?
Verifiable	a finite test, inspection or analysis can decide whether it is met	Does every predicate have a measurable boundary?
Understandable	its intended reader recovers the meaning without excessive inference	Is the composition simple, the vocabulary expected, the embedding shallow?
Singular	it states one independently testable obligation	Does coordination (“and”, “or”, “as well as”) join separate propositions?
Complete	it carries everything needed to define the behaviour in scope	Are the semantic roles filled: actor, trigger, object, condition, constraint?

The criteria are related but not the same. A requirement can be unambiguous and still hard to understand, and a sentence can be easy to read while allowing several readings.

Examples for each criterion

Unambiguous. “The system displays the user’s account details and transactions when they are updated.” Does they refer to the details, the transactions, or both? Better: “The system displays the updated account details and updated transactions whenever either is modified.” (The exact trigger still needs specifying if it matters.)

Understandable. “The system shall effectuate the subsequent invalidation of credentials upon the occurrence of a qualifying authentication failure.” Better: “The system shall invalidate the credentials after a qualifying authentication failure.” Same meaning, simpler words and structure.

Singular. “The system shall authenticate users and record all failed login attempts” holds two obligations that can pass or fail separately: authenticating users, and recording failed attempts. Singularity counts obligations, not sentences or clauses. A compound sentence can describe one tightly integrated behaviour.

Complete. “The system shall lock the account after failed login attempts.” How many attempts? Within what time? For how long? Better: “The system shall lock a user account for 15 minutes after five consecutive failed login attempts within a 10-minute period.” Completeness is relative to scope: the requirement needs the information that defines its behaviour, not every implementation detail.

The Time Lock Test

The source. The Time Lock is a short story I wrote: an off-world Federation research station, rebels in orbit, and a team that has to lock its research away until help arrives. I gave a passage of about 4,000 characters (quoted at the end) to Gemini 3.1 Pro and asked for three system requirements. It returned:

Secure Encrypted Storage: The system must encrypt all critical research findings and store them within a physical time capsule located in the facility’s underground vault.
Payload Ingestion: The system must be capable of receiving and storing specific complex data types, including essential blueprints, the Ingegard algorithm, and confirming test data.
Timed-Release Mechanism: The capsule must utilize a cryptographic time-lock that denies access to the stored data for a specific, predetermined amount of time until allied forces can retrieve it.

The run. Each requirement went through the checker once, with the same passage as context. Each verdict took 15 to 30 seconds. The site allows three checks, so that was the whole experiment.

😱 Oh, dear! Every requirement failed!

Table 1. The checker’s verdict per criterion (✓ pass, ! warning, ✕ fail).

Requirement	Unambiguous	Verifiable	Understandable	Singular	Complete	Verdict
1 Secure Encrypted Storage	!	✕	✓	✕	!	FAIL
2 Payload Ingestion	✕	✕	✕	!	✕	FAIL
3 Timed-Release Mechanism	✕	✕	!	!	✕	FAIL

That’s 1 pass, 5 warnings and 9 fails in 15 checks. None of it is surprising: these are sentences from a story, lightly dressed as requirements by another AI, and stories don’t specify key lengths. What matters is whether the reasons are right, and mostly they are:

A real syntactic ambiguity. “Confirming test data” can be read with confirming as an adjective (data that confirms something) or as a verb (the act of confirming the test data). That’s a textbook attachment ambiguity, and the checker named both readings.
It used the context. It noticed that “allied forces” is never tied to the “Federation forces” of the passage. It also took names from the story for its rewrites: Facility End-of-Life Protocol 2B and the Timed-Release Cryptographic Capsule.
The time lock. For requirement 3 it objected that “until allied forces can retrieve it” is unverifiable, “since the capsule has no way to observe or confirm that retrieval is now possible”. That is exactly the property of a cryptographic time lock: it can count time, it can’t observe events. My Block Time Lock post argues the same from the cryptography side.
Criteria overlap. One defect is often reported under more than one criterion. “Critical” is undefined appears under Unambiguous and Verifiable, and the missing actor under Unambiguous and Complete. Requirement 1 has five distinct defects (no actor, “critical” undefined, no encryption strength, two obligations, no trigger) spread over four criteria. The number of ✕ marks is not the number of problems.

The checker’s full answers

Quoted from the checker’s output, unedited.

Requirement 1: FAIL. The requirement bundles two separate obligations (encrypt, then store) under one unnamed actor, and gives no measurable criteria for what counts as “critical” or what encryption strength is required.

! Unambiguous: “The system” does not identify which subsystem is responsible for the encryption and storage action, leaving the actor open to interpretation. “Critical research findings” is also undefined, so a reader cannot tell which findings are in scope versus out of scope.
✕ Verifiable: No encryption algorithm, key length, or strength is specified, so “encrypt” cannot be checked against a concrete standard. There is also no measurable boundary for “critical,” making it impossible to verify which findings must be included.
✓ Understandable: The sentence is short and its intent – encrypt findings and place them in a physical vault capsule – is clear on a single read.
✕ Singular: The requirement joins two distinct obligations with “and”: encrypting the findings and storing them in a physical time capsule. These are separable actions that could be tested and fail independently, so they should be stated as separate requirements.
! Complete: No trigger or precondition is given for when this encryption and storage must occur (e.g., upon activation of an end-of-life protocol), even though the surrounding context implies one exists. The responsible actor is also left as “the system” rather than a named component.
Suggested rewrite: When ⟨Facility End-of-Life Protocol 2B⟩ is initiated, the ⟨Time-Lock Capsule System⟩ shall store all critical research findings in encrypted form, using ⟨encryption-algorithm⟩, within the time capsule located in the facility’s underground vault.

Requirement 2: FAIL. The requirement lists an open-ended, undefined set of data types using vague qualifiers like “specific complex data types” and “confirming test data”, and it names no verifiable criteria such as size, format, or time bound for the ingestion action.

✕ Unambiguous: The phrase “specific complex data types, including” signals a non-exhaustive list, leaving the reader unsure what other types might be covered. “Confirming test data” is syntactically ambiguous: it could mean data that confirms something, or the act of confirming test data. “The Ingegard algorithm” is also an undefined term with no stated meaning or boundary for what it encompasses.
✕ Verifiable: “Must be capable of receiving and storing” sets no measurable acceptance criteria: no size limit, format, retention duration, or error handling is specified. There is no way to design a finite test or analysis that would conclusively pass or fail this requirement.
✕ Understandable: A new engineer cannot determine what counts as “essential blueprints” or what “the Ingegard algorithm” is without external explanation, since neither is defined in the requirement or as a standard signalling term. The requirement reads as a narrative instruction rather than a precise technical statement.
! Singular: The requirement bundles two actions, “receiving and storing”, together with three distinct payload items (“essential blueprints”, “the Ingegard algorithm”, “confirming test data”), which could each warrant separate, independently verifiable requirements.
✕ Complete: No actor is explicitly named as responsible for ingestion (presumably “the system” refers to the Timed-Release Cryptographic Capsule, but this is not stated), and no trigger or precondition for when ingestion occurs is given. The open-ended list via “including” also leaves the object of the requirement incompletely specified.
Suggested rewrite: When the operator submits the payload for the Timed-Release Cryptographic Capsule, the ⟨Capsule Ingestion System⟩ shall receive and store exactly the following data items: ⟨blueprint files⟩, ⟨Ingegard algorithm file⟩, and ⟨test data files⟩, each not exceeding ⟨maximum size⟩ in ⟨required format⟩.

Requirement 3: FAIL. The requirement conflates two different release conditions (a fixed duration and an external event) without specifying either, and uses vague, unverifiable terms like “specific, predetermined amount of time” and “can retrieve it.”

✕ Unambiguous: The phrase “for a specific, predetermined amount of time until allied forces can retrieve it” gives two different release conditions - a fixed duration and an external event - without saying which governs or how they relate. “allied forces” is also never tied to the “Federation forces” mentioned in the surrounding narrative, so it is unclear whether these are the same actor.
✕ Verifiable: No numeric value or unit is given for “a specific, predetermined amount of time,” so there is nothing to test against. “until allied forces can retrieve it” is also unverifiable, since the capsule has no way to observe or confirm that retrieval is now possible.
! Understandable: The sentence mixes a design mechanism (“cryptographic time-lock”) with narrative-style rationale (“until allied forces can retrieve it”) rather than stating a plain observable behaviour. A reviewer unfamiliar with the story context would not know what event or value actually ends the lock.
! Singular: The requirement bundles two distinct obligations: denying access for a fixed duration, and denying access until an external party can retrieve the data. These are two different release conditions and should be stated as separate, unambiguous requirements.
✕ Complete: The requirement does not state the actor who sets or triggers the time-lock, the starting event for the countdown, or the actual duration value, leaving the precondition and object underspecified. “allied forces” is also not defined anywhere as an actor the capsule can recognize.
Suggested rewrite: When the capsule is sealed by ⟨responsible actor⟩, the capsule shall deny access to the stored data until ⟨duration value and unit⟩ has elapsed since sealing.

The Shape of a Rewrite

All three suggested rewrites follow the event-driven pattern of EARS, the Easy Approach to Requirements Syntax [1]: When ⟨trigger⟩, the ⟨system⟩ shall ⟨response⟩. Everything the checker didn’t know stays in angle brackets: the actor, the algorithm, the duration. That’s a good habit. A placeholder can’t be mistaken for a fact, while an invented value can.

🤔 Hold on, mate! Who’s Checking the Checker’s Suggested Rewrites?

When we put each suggested rewrite next to its own critique, three gaps appear:

Requirement 1 keeps “critical”. The critique says “critical research findings” is undefined and has no measurable boundary. The rewrite still says “all critical research findings”, with no placeholder. (It did deal with the two bundled obligations neatly: “store … in encrypted form” is one obligation.)
Requirement 2 keeps “receive and store”. The Singular warning names “receiving and storing” as two bundled actions. The rewrite says “shall receive and store”.
Requirement 2 introduces “the operator”. Unlike every other unknown, this actor isn’t in angle brackets, and nobody called the operator appears in the story; Dr. Rae and her team load the capsule. An assumption is presented as a fact.

And here’s something I found very interesting👇:

Requirement 3 drops the story’s intent. The critique says the requirement mixes two release conditions, a duration and an event, and should state them separately. The rewrite keeps only the duration and drops “until allied forces can retrieve it”. For a time-lock puzzle that is the right engineering answer, since a duration is the only thing it can enforce. But it’s a design decision the requirement’s owner should make, not one the checker should make quietly.

None of these makes the checker wrong about what’s wrong. They show that diagnosing a requirement and rewriting one are separate tasks, and the second has to be checked against the first. Still an important lesson!

This is getting meta - checking the checker?

I know, right? Please bear with me. Since we don’t know how the requirement checker works under the hood, we have to assume that the cherckers’s own output can have the exact problems it is tasked to look for. The gaps above kind of hint at this risk imo. Now, a rate limit of three checks rules out any statistical analysis (the web page only allowed for three requirement checks), but checks that need no ground truth are easy to highlight:

Round trip. Fill in the placeholders of a suggested rewrite and check it again. It should pass, or at least lose the criteria it was written to fix. Cost? Cheap.
Seeded defects. Start from a requirement that passes. Introduce one defect at a time (an ambiguous pronoun, a second obligation joined by “and”, a missing unit) and see whether exactly the matching criterion fails. Cost? Less cheap.
Paraphrase invariance. Reword a requirement without changing its meaning. The verdict shouldn’t change. Cost? Somewhere inbetween.
Repeat runs. Check the same requirement twice. A language model can answer differently, and a verdict that flips isn’t a verdict. Cost? Super cheap to do, but the scope of handling discrepancies feels unbounded.

Darling, would you mind morphing the meta?

Okay, so these are metamorphic tests we’re doing: checking relations between answers rather than the answers themselves, so we don’t need a gold standard in the form of an oracle. If I’m not mistaken, that’s the same idea as Prover’s own position on AI as a tool: “Generate, but verify!” - the AI’s output is trusted, but only after a check is done that does not depend on it [2]. Which makes total sense to me, but given how absolutely amazing today’s AI are, feels like something that is easy to gloss over, or even forget.

By the way, the concept of semantic mutation metric is something I want to read up - and once I’ve done so, I hope to return to this section with a better understanding of these things.

This…post…is clearly not “research”

No. It’s not. The circumstances (rate-limited to three attempts) made any rigorous testing impractical. Despite that fact, I had a lot of fun playing with the Prover Req Quality Checker. That being said - these following conditions made the test incomplete:

Three requirements, one run each. No rate, error or consistency estimate is possible.
No control. I never gave it a good requirement, so I can’t say whether it ever passes one. A checker that fails everything would have produced the same table.
Story requirements. Extracted from fiction by another AI, they were bound to be weak. Real requirements are a harder test.
One reader’s judgement. “Fairly”, “real ambiguity” and “the gaps” are my reading of the answers, not a measurement.

😂 Dude, I don’t think anyone is still reading this…novel.

Thanks and Disclosures

Thanks to Prover for putting this interesting tool online for anyone to play with, for free. I have no affiliation with Prover, and this post isn’t paid for. I’m learning by messing about with interesting technology. Was AI used in creating this post? Absolutely. I wrote an extensive draft by hand (because I love to write). And then I spent considerable time molding generated parts into a pleasant shape. Also - and I was somewhat reluctant to write this - some people may view a “review” of this sort as critique of Prover the company - it’s not. I just wanted to try out their cool technology and learn something new. Prover is a very exciting company in my oppinion. AI is growing exponentially - and so is the need to tame its hallucinatory tendencies - a challenge that I think companies like Prover are perfectly well equipped to take on.

Thanks for reading!

Appendix The Context Passage

The following passage from The Time Lock was given to the Prover Req Quality Checker as context.
The passage is from this short story and can be read here on the blog.

Dr. Angela Rae was head of Space Folding Research at The Periphery, a Top Secret remote Federation research facility located on the surface of a small moon at the outer fringe of the Kalix system. She and her 20-something-sized team of researchers were working as fast as they possibly could. A single thought racing through everyone’s mind - “How did they find us?”.

Up there, orbiting at a chill 26,000 miles, was death. Having covertly decelerated in the radar shadow of a nearby moon, the tiny Rebel space ship suddenly emerged less than an hour ago, catching every living soul on this outer-rim secret research facility by surprise, spreading fear among its few inhabitants. Wasting no time, the rebels immediately communicated their terms: stand down all defences, halt all interstellar communication, and prepare to be boarded.

With the hostile rebellion force in orbit, and a likely extermination of all Federation members of this facility, Dr. Rae and her team were frantically gathering all the key discoveries of advanced Space Folding technology that she and the team had made over the last decade. Realizing the danger of having ground-breaking space-faring technology end up in enemy hands, Angela Rae decided to initiate Facility End Of Life Protocol 2B: “Time-Lock Puzzle”. The protocol instructed Angela to encrypt all research findings into a time capsule located in the underground vault below the facility.

How did they find us? The thought was stabbing at the back of Angela’s mind, while she frantically navigated authorization steps of top secret subprocesses. This moon isn’t even registered in the Federation Naval Charts - it doesn’t exist. Do we have a spy on our team?

Allowing the terrifying thought to linger in her mind, Angela faced the group of researchers gathered around her in the Periphery’s Command Central - a grandiose name for a small room littered with computers.

“Everyone, listen up! There is zero chance that Federation forces will reach us in time - we’re on our own. None of us expected this, and I have as many questions as you do. In accordance with Federation Regulation, I have decided to initiate the creation of a Timed-Release Cryptographic Capsule. We need to hurry and prime its payload with all essential blueprints, the Ingegard algorithm, and confirming test data. If we don’t get the capsule ready and locked within the next hour then everything we’ve worked for risks falling into the wrong hands. That could mean the end of the Federation as we know it. I understand this isn’t the way any of us expected things to end. I want to extend my sincere gratitude to each and every one of you.”

Angela hesitated for a moment, but then decided to follow dictum, and with a straight face exclaimed.

“The Federation thanks you for your sacrifice.”

The research compute room fell silent, its heavenly-white focus-friendly interior decoration creating a mockery of the grim situation the team was facing. The faint sound of busy compute-hardware carelessly whirring in the background sent chills through Angela’s spine. Her last statement clearly drove home the message, no one in this room will be alive in a couple of hours.

The team’s predicament, Angela realised, was the delicate challenge of keeping top secret research out of Rebel hands, until Federation forces return on their scheduled re-supply mission. On the flip side, locking the research away for an indefinite time would place it too far out of Federation scientists’ reach, in a war that the Federation is currently losing.

What was needed, which some Federation geniuses on Earth had realised upon building the station, was technology to lock away invaluable research secrets for just enough time until Federation forces would return and retake control of the facility.

What was needed, was to send a message into the future.

References

A. Mavin, P. Wilkinson, A. Harwood, M. Novak, “Easy Approach to Requirements Syntax (EARS)”, 17th IEEE International Requirements Engineering Conference (RE'09), 2009.
Prover Technology, “CENELEC is amending EN 50716 for AI. Here is what the draft says”, 16 September 2026. https://www.prover.com/company-news/cenelec-is-amending-en-50716-for-ai-here-is-what-the-draft-says/