Fail Every Call: Borrowing from Formal Verification to Refactor Safely

Claude drafted this from my work notes and the session that did the work, and I edited it until it sounded like me. The decisions in it are mine.

Big refactors are risky when nobody has a record of what the code actually does. At work we run a few dozen long-running workflows on Azure Durable Functions, and more than half of them have no workflow-level tests. Without that record, a bug fix or a performance change is a guess, and so is any cleanup of the architecture.

The worst of them copies a customer database from one place to another. It’s one of our largest and longest-lived workflows, it has more branches than anything else we run, and its whole test file is commented out. In one Claude Code session I rebuilt it from scratch, then showed the rebuild does the same work as the old one, first in a test harness and then in 20 live runs against real Azure.

What made that safe is an idea borrowed from formal verification: write down what the code must always do, then check every case. Along the way it found six bugs in code that’s running today. None of the rebuild has shipped yet. It sits behind a flag that’s off everywhere.

Proving code instead of sampling it

Most testing checks examples. You pick some inputs, run the code, and confirm the outputs look right. The bugs live in the inputs you didn’t pick.

Formal verification flips that around. You write down a property the code must always hold (“this program never crashes”, “every lock taken is released”), then you prove it holds for every possible input and every path through the code. A machine checks the proof, so it doesn’t depend on anyone’s reading of the code being right.

Writing those proofs by hand takes specialists and a LOT of time, which is why it has mostly lived in chip design, aerospace and cryptography.

The part of Anthropic’s work you can steal

Anthropic’s formal verification write-up shows Claude doing that work at scale. For 239 fuzz entry points across 123 open-source libraries, it proved that the compiled RISC-V binaries always exit normally on inputs under 64 MB. The proofs come to about 180 million lines of Rocq, and the process found hundreds of real bugs along the way. I’m not going to pretend I understand what Rocq is or what a RISC-V binary is, but there are some high-level ideas in there that apply to normal application code.

The proofs themselves don’t fit a .NET workflow. They prove memory safety and crash freedom in compiled native code, and the CLR already gives you memory safety. My bugs were a different kind: ordering and cleanup bugs, like a release that never runs because the one before it threw.

So I kept the method and dropped the proofs. State the properties the code must hold, then check every case instead of the ones you happened to think of. For the copy workflow I wrote down three:

1. Every path, success or failure, gives back everything it acquired: firewall rules, group memberships, resource locks, temporary databases.
2. A customer never ends up with neither the old database nor the new one.
3. Two jobs never run at once for the same customer.

My version is cheaper and weaker than a proof. Fail every call the workflow makes, one at a time, and check that the properties still hold after each failure. Record what the old code does before changing it and hold the new code to it. Break the code on purpose to make sure the checks notice. Then hand the result to reviewer agents that haven’t seen your reasoning.

In the harness, property 1 is a loop and a count. The sweep fails each call in turn, then checks that every resource the run acquired was given back exactly once:

for (var failAt = 1; failAt <= callCount; failAt++)
{
    var context = await RunAsync(scenario, c => c.FailsNthCall(failAt));
    violations.AddRange(Violations(scenario, context));
}

Assert.True(violations.Count == 0);

// inside Violations, one of these per resource
Expect("group membership",
    acquired: run.Scheduled(nameof(GrantAccess)),
    released: run.Released(nameof(RevokeAccess)));

It isn’t a machine-checked proof, but it’s the same move: name the properties, then check every path instead of trusting someone’s reading of the code. The limits are real (one fault at a time, scripted Azure, no concurrency), and a TLA+ model is how you’d push past them. TLA+ is a language for writing down how a system is designed to behave, and its model checker tries every order things could happen in to find a broken property.

You can’t refactor what you never recorded

A refactor is only safe if you know what the code did before. Most legacy workflows don’t have that, so any change to them, including a bug fix or a performance improvement, is a change you can’t check.

Pinning behavior first fixes that. Once the old workflow’s behavior is recorded and its properties are written down, you can restructure it, fix it or speed it up, and the checks tell you exactly what moved. A difference is either one you meant (and you name it) or a regression.

That only works if the refactor and the fixes stay separate. Parity comes first, fixes come after, so every difference in the output traces back to one decision.

Failing every call

Durable Functions makes this easier than it sounds, because an orchestrator is deterministic code that schedules activities. A scripted test context can stand in for the runtime, answer every activity call, and record the order they came in.

1. Record the old workflow. The scripted context runs it through 11 scenarios and saves every call it makes to a file. A refactor that keeps behavior leaves those files unchanged.
2. Fail every call. For four scenarios, I reran the workflow once per call and failed that call each time, 177 runs in all, and checked the properties after each one.
3. Check the checks. Swapping two cleanup calls in the old code turned all 15 tests red, so the harness really does pin the cleanup order.

Step 2 is where the bugs came out. The old cleanup is a straight run of calls in a finally, and if one throws, everything after it is skipped, with the resource locks last. On a copy that has already succeeded, one failing firewall cleanup leaves both environments’ locks off and marks the job failed.

Failing call	Old workflow	New workflow
First cleanup call, after the copy succeeded	Throws. The firewall rule, group membership and both environments’ locks never come back.	Runs the rest of cleanup, notes the failure, and the copy stays succeeded.
Copying the restored database to the target	Deletes the target but leaves the temporary database behind.	Deletes both.
Closing the job	Deletes the finished copy.	Keeps it.

Across the whole sweep, 105 of the old workflow’s single-failure runs broke a property. The new one broke none. The other three bugs came out of reading the sweep against the code, and the worst of them is a replace that deletes the customer’s database before the copy even starts.

A rebuild that gives back everything it takes

We’d been iterating on a new shape for workflows at work. Each one is a list of declarative steps, so you can read it top to bottom, tell what it does without tracing it, and change one step without touching the rest. I’d tried it on a smaller workflow first, then chose to finish the iteration on the copy workflow as a real stress test.

The rebuild is a plan where each step is one small class. It adds a cleanup stack, where every step that acquires something registers how to give it back, and every release runs even when another one fails. Locks go back last, because they block the deletes the other releases make.

The old cleanup is a run of awaits in a finally, so the first one that throws skips the rest:

finally
{
    await context.CallActivityAsync(nameof(DisablePublicEndpoints), job);
    await context.CallActivityAsync(nameof(RevokeAccess), job);
    await context.CallActivityAsync(nameof(RemoveFirewallRule), job);
    await context.CallActivityAsync(nameof(RestoreLocks), sourceId);
    await context.CallActivityAsync(nameof(RestoreLocks), targetId);
}

In the new one, each step pushes its own release before it acquires anything, and the runner tries every release even when one fails:

// in the step that deletes the source locks
run.Cleanup.ReleaseLast(new RestoreLocks(run.Request.SourceId));

// in the runner, after the plan
foreach (var entry in cleanup.Due(planFailed))
{
    try
    {
        await InvokeAsync(entry.Step, run);
    }
    catch (Exception ex)
    {
        failures.Add(new CleanupFailure(entry.Name, ex));
    }
}

It’s a new workflow rather than an edit of the old one. Changing a durable orchestrator in place breaks every instance already in flight, and untangling the old one would have been hell on earth anyway. So it sits behind a flag that defaults off, next to the old one, which stays untouched until cutover.

The rebuild is held to the old code two ways. The property sweep covers six scenarios, 252 single-failure runs plus about 1,200 runs where a cleanup call fails too. A parity check runs both workflows on the same scenarios and failures and compares what each one changes in the outside world. Every difference has to be on a named list of intended changes, and anything else fails the build.

The rebuild fixes three of the six bugs: the skipped cleanup, the leaked temporary database and the deleted finished copy. It keeps the other three exactly as they were, since each one changes what customers see and deserves its own decision after parity.

Fresh eyes found the worst bug

Reviewer agents that hadn’t seen my reasoning went over the new code, and they found things my own checks didn’t. A rollback stayed armed after the copy finished. A replace target that had already disappeared still failed the copy. A half-opened firewall rule leaked. An unguarded flag read could block every copy. All four are fixed.

They also broke the new code 16 ways on purpose, and my tests missed 10 of them. After a fix round, 15 of the 16 are caught. The one survivor is a catch block that can never fire, so the check exposed dead code.

The worst bug of the whole effort came from the review of the API in front of it, and it was in code that’s already deployed. A resource id with a dot segment in it could turn a database delete into a delete of the whole SQL server. The harness never would have found it, since it isn’t an ordering bug. That fix went out on its own.

20 live runs, no surprises from the new code

The harness scripts Azure, so the real question was whether the new workflow does the same work against the real thing. I ran both 20 times on two dev environments: every copy kind first (a live database, cross-environment, point in time, a deleted database, a long-term backup and a replace), then a failure injected at five points in the flow.

Every copy kind passed on both. In every pair, old and new made the same calls with the same inputs, apart from the two differences the parity check had already named and poll counts that follow how long Azure took.

The failure runs are where the two split, and they split exactly where the harness said they would:

Failure point	Old workflow	New workflow
After the locks are deleted	Cleans up	Cleans up
While polling the copy	Cleans up	Cleans up
In a post-copy step	Cleans up	Cleans up
A release fails	Skips the rest of cleanup. Locks stayed off for 16 minutes and the job said success.	Runs the rest, relocks, and notes “cleanup did not finish” on the job.
Point in time, after the temp database exists	Leaks the temp database and skips both relocks. Locks stayed off for about 90 minutes, until someone relocked by hand.	Deletes the temp database, then runs every release.

The point-in-time failure is the one the harness didn’t fully see coming. It knew the old workflow leaks the temp database, and it knew the new one refreshes a cache earlier. What it didn’t know is that the old refresh runs after the firewall rule is removed, so it can’t reach the database anymore, throws, and skips both relocks. The harness scripted that refresh as always succeeding, so it had no way to see it.

The live runs also found problems outside the workflow, in old and new alike, that no scripted test could. A failed poll leaves the copy running into an orphan database. Replace drops the target about 7 minutes before the copy is known good. Other teams’ automation puts locks back underneath running copies. Each of those is its own ticket now.

Five things I’d do again

Record first, change second. Pinning the old behavior before touching anything is what made every difference explainable. When the live runs came back, I already knew what each difference was and why it was there.

The bugs live in cleanup. A broken happy path gets noticed because someone is watching it. Cleanup after a failure doesn’t, and every bug the sweep found was there. You only find those by failing every call on purpose.

Check the checks. Breaking the code on purpose showed my tests missed 10 of 16 changes on the first pass. A green suite you haven’t tried to break doesn’t tell you much.

Get a read from someone who hasn’t seen your reasoning. The worst bug of the whole effort came from a reviewer agent like that, and it wasn’t the kind of bug my harness looks for.

Fakes assume things away. A scripted test is only as good as what it scripts, and the live runs caught something mine took for granted. Run the real thing before you trust the fake.

The same loop, one workflow at a time

The same four steps apply to every legacy workflow:

1. Record its behavior.
2. Fail every call and read what breaks. Each real bug gets its own ticket.
3. Build the new version behind a flag and hold it to the old one with the property sweep and parity check.
4. Cut over and delete the old one.

Steps 1 and 2 are cheap and pay off on their own, even before any rewrite. About 17 of our workflows have a cleanup finally like the one that failed here, so I expect the same class of bug to show up again.

TLA+ is where this goes when you need guarantees a scripted test can’t give. A spec of the design can check every recorded trace against it, so the model can’t drift from the code. The first place I’d point it is the job queue, where a per-customer guard checks and then starts a job as two separate steps. That could break property 3 under concurrency, and a scripted test will never show it.

None of the ideas here are new. Write down what the code must always do, break it on purpose, check every path. It just cost too much to do by hand on a workflow this size, so nobody asked for it.

That’s the part I keep coming back to. The ceiling on this work wasn’t the model, it was the size of the ask. Ask for the outcome instead of the task, and never let the agent grade its own work. Formal verification is what that judge looks like for a refactor. Once you have one, the work you’ve been putting off for years stops being too big to start.