Formal Methods for Spec-Driven Development: Catching Requirement Conflicts as Products Evolve

A minimal example: adding trash and restore to a document app

Part 2 of a series on formal methods in requirements engineering. Part 1: Your .md File Is Not a Specification.

A document app lets users create documents with unique names and delete them. The product manager asks for a familiar feature: make deleted documents recoverable. Here is the requirements change.

  R1: THE SYSTEM SHALL allow a user to create a document with a name.
  R2: IF a user creates a document with a name already used by another document,
      THEN THE SYSTEM SHALL reject the request.
- R3: WHEN a user deletes a document, THE SYSTEM SHALL remove it.
+ R3: WHEN a user deletes a document, THE SYSTEM SHALL move it to the trash.
+ R4: WHEN a user restores a document from the trash,
+     THE SYSTEM SHALL restore it as it was before deletion.

One line changed, one line added.

Is there a problem? Before reading on, see if you can spot one.

In the previous post, we used formal analysis to find requirement gaps: requirements that weren't testable, and behaviors they never specified. This post is about a different problem, consistency: requirements that are each reasonable but can't all be true at once. And specifically, how these conflicts sneak in when a product changes.

Like Part 1, this is a minimal example. It's a classic that most developers and product managers have run into in a PRD at some point, and that's deliberate: when the problem is familiar, you can check the model checker's answer against your own experience.

Formal methods are usually associated with complex distributed systems and concurrency bugs. This example has neither: one user, one action at a time, a plain CRUD app. Yet this requirements hide bugs that are hard to see, but a few lines of formal specification can find in seconds. What makes formal methods useful isn't how complex the system is, but how many requirements interact, and even simple products have plenty of those.

Version 1: hard delete

Start with the app before the change. Users create documents with unique names and delete them. Deleting removes the document for good.

To keep the example small, the requirements cover only creating and deleting documents, and in version 2, the trash and restore. Reading, updating, and listing documents are out of scope, as are emptying the trash and permanently deleting old items. We'll come back to those last two when we look at the product decision.

The version 1 requirements:

R1: THE SYSTEM SHALL allow a user to create a document with a name.
R2: IF a user creates a document with a name already used by another document,
    THEN THE SYSTEM SHALL reject the request.
R3: WHEN a user deletes a document, THE SYSTEM SHALL remove it.

Here is the FizzBee spec. If you read Part 1, the structure will look familiar: a User role performs actions, and a System role holds the state.

▶ Open in FizzBee Playground

NAMES = symmetry.nominal("name", 2)
IDS = symmetry.nominal("id", 3)

role User:
    atomic action Create:
        name = oneof NAMES.choices()   # a name in use, or a fresh one
        system.create(name)

    atomic action Delete:
        id = oneof system.docs
        system.delete(id)

role System:
    action Init:
        self.docs = {}   # id -> name

    atomic func create(name):
        require name not in self.docs.values()   # R2
        self.docs[IDS.fresh()] = name

    atomic func delete(id):
        self.docs.pop(id)                        # R3

action Init:
    user = User()
    system = System()

One new piece of FizzBee: symmetry.nominal. We don't care what names or IDs actually are, only whether two of them are equal. A nominal gives us a small, bounded pool of interchangeable values. fresh() allocates an unused one, and choices() offers every value currently in use plus one fresh value, if the pool isn't exhausted. When fresh() can't allocate, that step is simply disabled, which keeps the state space finite without extra bookkeeping. With 3 IDs and only 2 names, version 1 always has a spare ID for a new document. (Details in the docs.)

Two kinds of properties

The first property is R2, stated over states instead of the create action: no two documents ever share a name. In version 1, create is the only way to make a document, so the two say the same thing.

always assertion UniqueNames:
    names = system.docs.values()
    return len(names) == len(set(names))

This is a safety property: something bad never happens. Safety properties have a blind spot. A system that does nothing never violates them. A create that rejects every request satisfies UniqueNames perfectly.

So we add a second property, of a different kind. A classic bug in systems with unique names is a delete that forgets to free the name, for example by leaving a row behind in a unique index. The user deletes "report.pdf" and can never create "report.pdf" again. To rule that out, we say a good thing is always possible:

# Any name not used by a document can be used to create a new one
always assertion FreeNamesUsable:
    for name in NAMES.choices():
        if name in system.docs.values():
            continue
        created = [n for n in next_states()
                   if name in [n.state.system.docs[i] for i in n.state.system.docs
                               if i not in system.docs]]
        if len(created) == 0:
            return False
    return True

From every reachable state, for every name not in use, there must be a next step that creates a new document with that name. next_states() lets us look one step ahead from the current state. Creating a document is a single step here, so one step is enough; a multi-step flow, like a confirmation dialog, would need to look further ahead.

Open the spec in the FizzBee Playground and click Run. Both properties pass. Version 1 is fine, and we ship it.

Version 2: trash and restore

Now apply the requirements change. R1 and R2 stay the same:

- R3: WHEN a user deletes a document, THE SYSTEM SHALL remove it.
+ R3: WHEN a user deletes a document, THE SYSTEM SHALL move it to the trash.
+ R4: WHEN a user restores a document from the trash,
+     THE SYSTEM SHALL restore it as it was before deletion.

In the spec, delete moves a document from live to trash, and a new restore action moves it back.

▶ Open in FizzBee Playground

  role System:
      action Init:
-         self.docs = {}
+         self.live = {}    # id -> name
+         self.trash = {}   # id -> name

-     atomic func delete(id):
-         self.docs.pop(id)
+     atomic func delete(id):                     # R3 (changed)
+         self.trash[id] = self.live.pop(id)
+
+     atomic func restore(id):                    # R4 (new)
+         self.live[id] = self.trash.pop(id)

The User role gets a matching Restore action, and the ID limit moves into a constant, ID_LIMIT = 3, used below. The full v2 spec is in the playground link above.

create is unchanged: it still checks the name against live documents only, so a deleted document's name can be reused, just as in version 1. (R2 says "another document"; like version 1, we read that as another live document.)

To check the new requirement R4, we add two properties. First, a trashed document must be restorable, from any state. That's a possibility property, the same kind as FreeNamesUsable:

always assertion TrashedDocsRestorable:
    for id in system.trash:
        if len([n for n in next_states() if id in n.state.system.live]) == 0:
            return False
    return True

Second, it comes back "as it was before deletion." In our model, the only thing a document has is its name, so: a document keeps its name on its way into the trash, stays in the trash unchanged until it's restored (we left out emptying the trash), and comes back with the same name. As in Part 1, a transition assertion compares each pair of consecutive states:

transition assertion RestoredAsBefore(before, after):
    for id in before.system.trash:
        name = before.system.trash[id]
        if id in after.system.trash:
            # a trashed document stays in the trash, unchanged...
            if after.system.trash[id] != name:
                return False
        elif after.system.live.get(id) != name:
            # ...or comes back with its old name
            return False
    # delete keeps the name
    for id in before.system.live:
        name = before.system.live[id]
        if after.system.trash.get(id, name) != name:
            return False
    return True

It says nothing about live documents, which leaves room for a future "rename" or "edit" action.

The v1 assertions carry over, with docs becoming live. In FreeNamesUsable, "a new document" now has to mean a new ID, not a restored one, so it excludes IDs already in the trash. (It also skips states where every ID is in use, since no create is possible there; that's a bound of the model, not a requirement.)

always assertion FreeNamesUsable:
    if len(system.live) + len(system.trash) >= ID_LIMIT:
        return True
    for name in NAMES.choices():
        if name in system.live.values():
            continue
        created = [n for n in next_states()
                   if name in [n.state.system.live[i] for i in n.state.system.live
                               if i not in system.live and i not in system.trash]]
        if len(created) == 0:
            return False
    return True

Run the model checker

Open the full v2 spec in the FizzBee Playground and click Run. The model checker reports that the v1 assertion UniqueNames fails:

A user deletes "report.pdf", creates a new "report.pdf", then restores the old one. Two documents now have the same name.

Some of you may have spotted this at the start of the post, and may have seen it in a real project. It's a very common issue. But real requirements span many pages, tickets, and versions, and the two that conflict are rarely on the same page. That's where a mechanical check matters most.

Notice that the failing check, UniqueNames, was written for version 1. Like a regression test, it caught a problem nobody thought to look for.

Fix attempt 1: refuse to restore on conflict

The obvious fix is a precondition, the same move that worked in Part 1:

▶ Open in FizzBee Playground

    atomic func restore(id):
        require self.trash[id] not in self.live.values()   # <-- new
        self.live[id] = self.trash.pop(id)

UniqueNames passes now, but TrashedDocsRestorable fails at step 3 of the same trace:

live = {id1: name0}, trash = {id0: name0}

The old "report.pdf" can't come back. We didn't fix the bug; we swapped a duplicate name for a document stuck in the trash. This is the do-nothing blind spot from version 1: refusing to act made the safety property pass, and only the possibility property noticed.

Fix attempt 2: reserve names in the trash

Try it the other way. Don't let anyone take a name that belongs to a trashed document:

▶ Open in FizzBee Playground

    atomic func create(name):
        require name not in self.live.values()
        require name not in self.trash.values()  # <-- new
        self.live[IDS.fresh()] = name

Restores never conflict now, so UniqueNames and TrashedDocsRestorable both pass. But FreeNamesUsable, the property we wrote in version 1 to catch names that never get freed, fails:

live = {}, trash = {id0: name0}

No live document is named "report.pdf", yet the user can't create one. From version 1's point of view, this is exactly the bug that assertion was written to catch.

It's the requirements, not the model

Two more fixes are possible: restore the old document under a new name, like "report (1).pdf", or overwrite the newer document with the restored one. Here is how every approach does:

Only overwrite keeps the four properties we wrote, and it loses the user's data: the newer "report.pdf" is gone. Nobody wrote "don't lose data" down, because it's too obvious to say. Add it as a requirement, and every option gives something up: the first four each break one of our properties, and overwrite breaks the new one. The requirements need a product decision.

Notice that, until we wrote the overwrite fix on purpose, none of our specs overwrote anything, even though no property forbade it. The actions did: restore moves one document, and everything it doesn't touch stays the same. That's why a formal spec has two parts. The actions say what the system does, and they constrain the implementation even where nobody thought to write a rule. The properties say what must always be true, and the model checker checks the actions against them. Properties alone would have allowed the overwrite.

Proving that no other option exists, and finding unstated requirements like this one, needs a different kind of model. We'll cover that in the next post.

The product decision

Formal analysis can't tell you which requirement to give up. That's a product decision. What it does is turn a vague unease into a precise choice, with the trade-offs spelled out.

The first two options change the naming policy. The rest decide what happens at restore time.

Whichever you choose, the decision belongs in the formal spec. That's the version the model checker holds every future change to, and the one the code is built and tested against. The prose requirements change too, as the readable summary. For example, choosing rename on restore, the prose becomes:

R2: IF a user creates a document with a name already used by another live document,
    THEN THE SYSTEM SHALL reject the request.
R4: WHEN a user restores a document from the trash,
    THE SYSTEM SHALL restore it as it was before deletion,
    except for its name as described in R4b.
R4b: IF a live document already uses the restored document's original name,
     THEN THE SYSTEM SHALL restore it under a new, unused name.

R2 now says "live," so the text matches what the spec has done since version 2.

In the spec, RestoredAsBefore now allows a name change on restore, but only when the old name is taken by a live document:

▶ Open in FizzBee Playground

transition assertion RestoredAsBefore(before, after):
    for id in before.system.trash:
        name = before.system.trash[id]
        if id in after.system.trash:
            if after.system.trash[id] != name:
                return False
        elif id not in after.system.live:
            return False
        elif after.system.live[id] != name and name not in before.system.live.values():
            return False                                    # R4b: rename only on conflict
    for id in before.system.live:
        name = before.system.live[id]
        if after.system.trash.get(id, name) != name:
            return False
    return True

And the code:

    atomic func restore(id):
        name = self.trash.pop(id)
        if name in self.live.values():
            name = NAMES.fresh()   # R4b
        self.live[id] = name

All four properties pass, and nothing is lost. (The model gets one spare name, symmetry.nominal("name", 3), so a rename never runs out of names.) The product decision is now an explicit, reviewable change to a property, rather than a quiet change in code.

Where the answer lives

In an example this small, a careful engineer would catch the problem in review, and a good coding agent would likely ask about it. The trouble is what happens to the answer. It ends up in a PR comment, a Slack thread, or a chat with the agent. The requirements doc still says "another document." Six months later, someone adds "archive" or "share with a team," and the same question comes up again, with nobody remembering it was already decided, or why.

Asking also depends on someone noticing. Here the two conflicting statements sit three lines apart. In a real product, R2 was written two years ago in a different document, by someone who has since left, and nothing about the trash ticket points back to it. Coding agents have the same problem in a new form: an agent working on the trash ticket sees only what's in its context. R2 may never get loaded, or it was read hours ago and summarized away when the context was compacted.

An executable spec handles both. The decision is recorded as an assertion, and the assertion keeps checking it on every future change. That's what happened here: UniqueNames and FreeNamesUsable were written for version 1, nobody thought about them during the trash change, and they caught the problem anyway. A .md file can't do that. Like a test suite for code, the spec remembers what everyone has forgotten, and it can run on every change. A coding agent can run the spec before and after its change, see a counterexample when an older property breaks, and raise it with the team before writing the code.

Summary

• Consistency asks whether any system can satisfy all the requirements at once.
• Formal methods aren't just for distributed systems. Even a single-user CRUD app can have conflicting requirements.
• Conflicts often appear when requirements evolve: words like "document" or "delete" change meaning, and older requirements are silently reinterpreted.
• An executable spec acts as a regression suite for requirements. Old assertions keep checking old promises after the change.
• Possibility properties ("it is always possible to restore") are essential. Without them, refusing to act passes every check, and a conflict looks like a fix.
• Passing every property you wrote doesn't mean nothing is missing. Overwrite passed all four. The actions are what kept our specs from overwriting.
• Coding agents need checks, not memory. An executable spec catches a broken older requirement even when the agent never saw it.
• When every fix gives up something you care about, stop fixing the model. The requirements need a product decision.

In the next post, we'll remove the actions and let the model checker search every possible implementation, both to prove when requirements are inconsistent and to find unstated requirements like NoDataLoss. After that, we'll look at testing an implementation against the spec with model-based testing, and at specifying UX properties.

Appendix: final spec (rename on restore)

The complete spec after the product decision. All four properties pass.

▶ Open in FizzBee Playground

# v3: rename on restore (product decision)
ID_LIMIT = 3
NAMES = symmetry.nominal("name", 3)   # one spare name for renames
IDS = symmetry.nominal("id", ID_LIMIT)

role User:
    atomic action Create:
        name = oneof NAMES.choices()
        system.create(name)

    atomic action Delete:
        id = oneof system.live
        system.delete(id)

    atomic action Restore:
        id = oneof system.trash
        system.restore(id)

role System:
    action Init:
        self.live = {}    # id -> name
        self.trash = {}   # id -> name

    atomic func create(name):
        require name not in self.live.values()   # R2 (another *live* document)
        self.live[IDS.fresh()] = name

    atomic func delete(id):                     # R3 (changed)
        self.trash[id] = self.live.pop(id)

    atomic func restore(id):                    # R4 (new)
        name = self.trash.pop(id)
        if name in self.live.values():
            name = NAMES.fresh()                # <-- rename on restore
        self.live[id] = name

action Init:
    user = User()
    system = System()

always assertion UniqueNames:
    names = system.live.values()
    return len(names) == len(set(names))

always assertion FreeNamesUsable:
    if len(system.live) + len(system.trash) >= ID_LIMIT:
        return True   # every ID in use: a modeling bound, not a requirement
    for name in NAMES.choices():
        if name in system.live.values():
            continue
        created = [n for n in next_states()
                   if name in [n.state.system.live[i] for i in n.state.system.live
                               if i not in system.live and i not in system.trash]]
        if len(created) == 0:
            return False
    return True

# R4: any document in the trash can be restored, from any state
always assertion TrashedDocsRestorable:
    for id in system.trash:
        if len([n for n in next_states() if id in n.state.system.live]) == 0:
            return False
    return True

# R4 + R4b: restored as before, except for a rename on conflict
transition assertion RestoredAsBefore(before, after):
    for id in before.system.trash:
        name = before.system.trash[id]
        if id in after.system.trash:
            if after.system.trash[id] != name:
                return False
        elif id not in after.system.live:
            return False
        elif after.system.live[id] != name and name not in before.system.live.values():
            return False                                    # R4b: rename only on conflict
    for id in before.system.live:
        name = before.system.live[id]
        if after.system.trash.get(id, name) != name:
            return False
    return True

Try it yourself: v1 · v2 · fix 1 · fix 2 · rename on restore · overwrite · v3 decision