From Behavior to Proof

A systems engineer sits down and describes how something should work. A user issues a command. The application opens a session, retrieves context, generates a model, asks an analyst to review it, commits the result, closes the session. It takes an afternoon, and it is the interesting part of the job.

Then the second afternoon starts. The same behavior has to be rewritten as requirements — one numbered shall-statement per step, each phrased carefully enough to survive a review. Then a third pass: verification cases, one or more per requirement, each explaining how anyone would ever know whether the requirement was met.

Three descriptions of the same thing, written by hand, in three notations. On a small system this is tedious. On a real one — thousands of behavioral elements, dozens of engineers, a decade of revisions — it is the single largest source of inconsistency in the entire program. Not because anybody is careless, but because nothing keeps the three copies in agreement. Change the behavior and two of the three quietly go stale.

The obvious response is to generate the requirements from the model. People have been doing this for years. And the output is disappointing in a way that takes a while to name.

Why generating requirements isn’t enough

Here is a derived requirement of the kind a straightforward transformer produces. It is correct. It traces perfectly. It is also useless:

The application shall retrieve the model context. require constraint { notEmpty(uc.'Retrieve Model Context'.context) }

Two things are wrong, and both are invisible if you only look at the model.

First, nothing can evaluate it. uc.'Retrieve Model Context'.context is a precise reference to a parameter of an action inside a use case. A running application does not expose that. There is no endpoint, no log line, no database column that corresponds to it. The expression is exact and unmeasurable. A test engineer handed this requirement has to invent an interpretation, and two test engineers will invent two.

Second, notEmpty is not a standard. It says something was produced. It says nothing about whether the right thing was produced. The model declared the parameter’s type; it never said what makes an instance of that type acceptable.

So the transformation succeeds and the program still gets requirements it cannot test. The generated artifact has the shape of rigor without the substance. That is arguably worse than writing them by hand, because it looks finished.

The question that changes the answer

The fix is not a better transformer. It is a different question.

Most requirement generation asks: what must the system do? The model already answers that. Restating it in shall-form adds ceremony, not information.

The question worth asking is:

What must I be able to see, and do, at the edge of this thing, in order to decide whether it did what it should?

Answer that and the requirements largely write themselves — and, more importantly, they land on ground a test can stand on.

Concretely, it means requirements stop referring to the model’s internals and start referring to an evidence record: a description of what one execution was observed to do. Before-state, stimulus, after-state, outcomes. The kind of thing a test harness, an API, or a structured log actually produces.

The same requirement, projected onto evidence:

WHEN Open Session has completed, the application shall retrieve the
model context.

assume  evidence.stateBefore == openSession
require evidence.stateAfter  == retrieveModelContext
require evidence.context
require evidence.contextIdMatches
require evidence.contextVersionMatches
require evidence.contextHashMatches

Every clause is something a harness can populate and a verdict can be computed from. Note the last three lines — we will come back to where those came from, because they are not something a use case can tell you.

Three properties, borrowed from hardware

Test engineers have known for decades that you cannot test what you cannot reach. Their vocabulary transfers cleanly, and it is the right frame for this whole problem.

Observable — can you see the outcome from outside the box? A fact is observable when it crosses an interface, travels through a port, or is a declared output of the use case. Everything else is inside the box, and someone has to deliberately publish it before any test can check it.

Controllable — can you drive the thing into the state you want to test? Every event the use case waits for, and every action a human actor performs, is a place where a harness can push. A use case with no waiting points and no human actors cannot be driven at all; it can only be started and watched.

Verifiable — is there a Boolean somebody can evaluate? Prose is context. The expressions are the deliverable.

Apply those three questions to a behavioral model, mechanically, and something unexpected falls out. The transformation does not just produce requirements. It produces a ledger of what you cannot see.

For a worked example I keep for exactly this purpose, that ledger reads:

controllable ........... 8      the harness can inject these
observable at boundary . 21     no new instrumentation needed
needs instrumentation .. 15     somebody must build a probe

Fifteen probes. That is a real number, arrived at before a line of code exists, while the architecture can still change. It is arguably more valuable than the requirements themselves — it is the testability cost of the design, quoted up front instead of discovered during integration.

Every hole in the box gets a name

“Crosses an interface” is doing a lot of work in that first definition, so it is worth saying what an interface is here. It is a port — the named feature through which something enters or leaves the subject. A use case can declare one:

action 'Await Command' accept c : Arch::Command via app.commandPort;

Most don’t, for most of their crossings. That is not a reason to leave the interface anonymous: something still enters, and an obligation that cannot say where is an obligation nobody can test. So name it after the payload, and say that you did:

info D12 — Boundary crossing has no declared port; one was synthesized so the
interface is still nameable. Using 'verificationModelPort'.

The name then holds everywhere it needs to: the port declared on the subject, the interface requirement that navigates it, the verification case that exercises it, and the documentation of the test driver method that pushes through it.

This matters more than it sounds. A boundary crossing is the cheapest thing to observe, because no probe has to be built for it. Naming them turns a diffuse claim — “these things cross the boundary” — into a concrete list of interfaces the architecture owes, which is exactly the kind of thing that gets forgotten until integration.

What a machine genuinely cannot derive

This is the part that most matters, and the part most tools skip.

You cannot get “never” from “sometimes”

A use case is an existential statement. It says: there is a path where this happens. Open a session, retrieve the context, generate the model.

A great many of the requirements a serious program needs are universal negatives. The system shall not submit the request when provenance cannot be confirmed. The system shall not present an invalid option.

No amount of cleverness derives the second kind from the first. This is not a limitation of any particular transformer; it is a fact about logic. If your model only describes what happens, no tool can tell you what must never happen.

The consequence is unavoidable and worth stating plainly: if you want prohibitions, you must model the circumstances under which they apply. The engineer draws the failure branch. Three lines:

#Exception #Terminal
action 'Record Context Retrieval Failure' { out contextFailureRecorded : Boolean; }

if 'Retrieve Model Context'.contextRetrieved then 'Generate Verification Model';
#Exception
else 'Record Context Retrieval Failure';

From that — plus one declaration that the model is complete, that any path it does not show is forbidden — a machine can write the prohibition, its constraints, and a verification case that exercises the failure deliberately rather than never.

That closing declaration matters. Without it, an unmodeled path is merely unspecified, not forbidden, and generating “shall not” would be putting words in the engineer’s mouth. You have to say it.

Two kinds of state

The second limit is subtler and catches people out.

A derived state machine has a state for each behavior, and each state means exactly one thing: this behavior is running now. It is true for one step and then it isn’t.

But some conditions persist across behaviors. A session is open. The system is degraded. The user is authenticated. These are states too — the difference is what owns them:

The use case is in a state. The subject holds other states.

A held state cannot be derived from a behavioral flow, and the reason is instructive. “A then B” says B follows A. It says nothing about which of A’s effects are still true while B runs. To infer one, a tool would have to decide, for every output, whether it latches or is transient:

action 'Open Session'             { out opened         : Boolean; }   // latches
action 'Validate Model Structure' { out structureValid : Boolean; }   // transient

Those two lines are syntactically identical. Only the engineer knows which is which, and a tool that guesses will be confidently wrong. So it should not guess.

Three more things only you can say

The same shape recurs. Each is information a behavioral model can hold but does not hold by default.

What good data looks like. A use case types its data; it never says what makes an instance acceptable. Declare the criteria once per item type and every parameter of that type gains real predicates instead of a bare presence check.

What the subject holds. Conditions that persist across many steps — a session is open, the system is degraded — are held by the subject, not entered by the use case. Declare them and guards over them resolve; leave them undeclared and the guard should be reported, never dropped.

What was handed in. Data supplied to the use case from outside is assumed, never required: the system is not answerable for producing what it was given, only for behaving correctly with it. That asymmetry between inputs and outputs runs through every derived artifact.

Failing loudly is a feature

There is a version of this system that is much worse than one that refuses to guess, and it is easy to build by accident.

Suppose a guard refers to a held state the model never declared — if sessionActive then commit. The tool cannot project that onto evidence. The tempting behavior is to drop the guard and carry on.

Do that and both branches of the decision become unconditional. The output still has every state, every transition, every requirement. It parses. It reviews well. And it permits more behavior than the engineer specified, with nothing anywhere saying so.

That is the most dangerous failure a derivation can have: silent weakening disguised as completeness. The right response is the opposite — name the reference, name the branches that lost their condition, raise a diagnostic, and print a loud block above the state machine in the generated output.

The general principle is worth extracting, because it applies far beyond any one tool: when an automated transformation cannot do something, the cost of silence is higher than the cost of noise. An error is recoverable. A confident, wrong, complete-looking artifact is not.

The sharpest example came from my own output

A generated end-to-end test could never have passed. It conjoined every per-step obligation over a single execution record, and each one fixes the use case state to a different value:

stateAfter == openSession
stateAfter == retrieveContext
stateAfter == generateModel
… twenty-one of them

One record holds one value. The suite compiled, listed, and looked complete.

It hid because the generated tests had only ever been run against the stub — where every test dies on the first unimplemented driver call, before reaching an assertion. A stub run proves a suite is well-formed and discoverable. It proves nothing about whether the assertions agree with each other.

The fix was a small piece of modeling discipline rather than a patch. Step ordering was already proven, because each per-step case assumes the state it starts from. What a whole-execution record can settle is now derived on purpose: the journey (every nominal step ran and no others), the destination, and the boundary crossings.

Correcting it surfaced two more defects the same way: a decision’s mutually exclusive branches were both being required, and a successful run was being asked to produce an output only the failure path emits.

What it produces

From one use case — about 346 lines describing an analyst-driven model generation and review workflow — the transformation emits a single self-contained package of roughly 2,100 lines containing:

Artifact	What it is
25 states	one per behavior, plus terminal states for success and handled failure
30 transitions	each naming what fires it, with guards from the decisions
an evidence schema	44 attributes, each classified by how a test would obtain it
34 requirements	including 3 prohibitions no use case could have yielded alone
28 verification cases	one per obligation, plus an end-to-end pass over the whole run
28 Playwright tests	one per verification case, against a generated driver interface
5 ports	every hole in the black box, named — including the two nobody named
an observability report	the 8 / 21 / 15 ledger from above

Every requirement is verified by at least one verification case. Every element traces. Identical input produces byte-identical output — the same file, to the byte, every time — which is what makes the result reviewable and auditable rather than merely plausible.

The most useful thing it said was “no”

Two older use cases were lying around, written before any of this existed. Running them through produced a result worth more than the requirements did:

Model	prohibitions	observable at boundary	needs instrumentation
the reworked example	3	21	15
older use case 1	0	0	14
older use case 2	0	0	22

Zero boundary-observable facts. Those two models, as written, specify nothing that a black-box test could ever check. No declared outputs, no failure paths, no acceptance criteria — all behavior, no evidence.

Nobody had noticed, because nothing had ever asked the question. The models looked complete. They had actions and flows and decisions, and reviewers had signed them off. It took a tool that insisted on testability to reveal that they described a system nobody could verify.

Finding that is the point. A tool that only ever produces output teaches you nothing.

Why this is deterministic, not generative

It would be very easy, today, to point a language model at a use case and ask it for requirements. It would produce something readable in seconds.

I did not do that, and the reason is a thesis rather than a preference.

A requirement is a contract. Its value comes from being stable, reviewable, and identical every time you ask. If the same use case yields subtly different requirements on Tuesday than it did on Monday, the traceability is theater — you cannot tell whether a change came from the engineer or from the generator, and nobody can sign anything.

So the transformation is a pure function. Same input, same output, byte for byte, verified across separate processes. No clock, no randomness, no unordered iteration reaches the result. Where judgment would be required, it emits a diagnostic instead of guessing.

That leaves plenty of room for AI, in the right place: helping an engineer build the model, reviewing it, spotting a missing failure branch, suggesting acceptance criteria. Judgment upstream, determinism downstream. The machine that writes the contract should not be the machine that improvises.

What actually changes for the engineer

An honest accounting, because the honest version is still a very good deal.

What does not change. The engineer still supplies every fact that ends up in the requirements. What counts as valid data. What must never happen. Which outcomes matter to the stakeholder. That information has to exist, and no tool can conjure it. Anyone promising otherwise is selling something.

What changes. You stop writing requirements and verification cases as documents. Each fact is stated once, in the behavioral model, in a form that is checkable. And then the machine guarantees the things people reliably fail at:

• every element has a requirement, and every requirement a verification case;
• every requirement is phrased consistently and traces in both directions;
• coverage and impact analysis are mechanical rather than archaeological;
• the off-nominal cases get tests, instead of being the ones everyone means to get to;
• and the whole thing regenerates, identically, when the model changes.

The second afternoon disappears. The third afternoon disappears. The first afternoon gets longer and more demanding, because now the model has to carry the failure paths and the acceptance criteria it always should have carried.

That is the trade, and it is the right one. The hard thinking moves earlier, where it is cheap, and stops being retyped into three notations, where it is expensive and error-prone.

Where this goes

The interesting frontier is not more generation. It is more honesty.

Every limit described above — the existential/universal gap, held states, quantitative performance, safety properties — is a place where a program currently believes it has a specification and does not. A tool that maps those gaps precisely, and refuses to paper over them, changes what a design review can be about.

Right now, a review asks: are these requirements well written? The better question, and the one this makes askable:

Is there anything here we could not test, and do we know why?