Formal Verification for Vue Developers: No Math Required

Your retry button has a bug.

You can’t see it in code review. Your tests pass. And your users find it after a reload.

I found it with formal verification. I know, that sounds like a math degree. It’s a program that tries every order of events in your app and tells you which one breaks.

Let me show you with a todo app.

It’s a todo list that saves in the background. Your change shows up at once, and the app sends it to the server:

// src/composables/useTodos.ts
const todos = ref<Todo[]>([])
const isSaving = ref(false)
const failed = ref<Todo[]>([])

async function add(text: string) {
  const todo = { text, done: false }
  todos.value.push(todo)
  isSaving.value = true
  try {
    await api.post('/todos', todo)
  } catch {
    failed.value.push(todo)
  } finally {
    isSaving.value = false
  }
}

async function retry() {
  const again = failed.value.splice(0)
  await Promise.all(again.map((todo) => api.post('/todos', todo)))
}

I’d approve this in a code review. It has an optimistic update, error handling and a retry.

Now imagine the server saves the todo, but the answer never reaches the browser.

The screen says “All changes saved”. The server has milk twice.

From the browser, “the request got lost” and “the answer got lost” look the same. Both are a failed fetch. On the server they’re the opposite.

I’d write a test for “save works”. I’d write one for “save fails, retry works”. Both are green.

But in my test, a failed save means the server got nothing. I never wrote the test for the lost answer, because I never thought of that order.

A test checks the orders you thought of.

A program can try every order for me. But this part confused me at first. I thought the tool reads my Vue files.

It doesn’t. It never sees them.

Think of a house and a floor plan. My composable is the house. For the checker, I draw a floor plan. It’s a second, tiny file that says what can happen and in which order. It has no fetch and no Vue.

There’s no import. The model doesn’t load my composable. I read my code and write the same idea again, much smaller.

The checker walks every route through the floor plan. It never enters the house.

That floor plan is called a model.

The model reimplements the behaviour of my composable, plus the server and the network around it.

Everything else stays out. No todo text, no reactivity, no URLs. A change is a number: 1, 2, 3.

It has two parts. First, the things that can change:

Second, the things that can happen. Here’s the start of add() in my code:

todos.value.push(todo)
isSaving.value = true
api.post('/todos', todo)

And here’s the same step in the model:

YouMakeAChange ==
  /\ made' = made + 1
  /\ inFlight' = inFlight \cup {made + 1}
  /\ isSaving' = TRUE

Read /\ as “and”. Read made' as “made afterwards”. And \cup adds something to a set.

So one more change exists, it’s on its way, and the spinner is on. Those are the same three lines, with Vue removed. I left out two lines of bookkeeping.

Now comes the interesting part. In my code, await api.post() is one line. In the model, it’s three events:

My catch block can’t tell the last two apart. The model can.

That’s why the model has to describe the server too. The bug isn’t in my 19 lines alone. It needs the server and the network to happen.

The model is a list of things that can change and things that can happen. That’s called a state machine.

• States are where you can be.
• Events are what happened.
• Transitions say which event moves you from which state to which.

I didn’t rewrite my code as one. My code already was one. I never drew it, so it was hidden in the refs.

Here’s the one I had in my head:

It has three states and four arrows.

Then the checker counted the real one. Every combination of isSaving, failed, inFlight and applied is a state. That’s 729.

The bugs are in the states I never drew.

That’s what a model checker does. You hand it the model and some rules, and it visits every state the model can reach.

There’s no math in that part. It’s brute force, like trying every combination on a bike lock:

1. Start with the first state, where nothing is made and nothing is in flight.
2. Try every event that’s allowed there.
3. Check all the rules on each new state.
4. Remember the new states, and skip the ones it has seen.
5. Repeat until nothing new shows up.

It tries all one-step paths first, then all two-step paths. So the first break it finds is also the shortest one.

The only math is in the notation.

A rule is a sentence that must be true in every state.

The language is called TLA+. A rule looks like this:

NoChangeIsSavedTwice ==
  \A change \in Changes : applied[change] <= 1

You don’t have to read that. \A means “for every”. For every change, the server applied it at most once.

And I didn’t write it. My coding agent did. My job was the sentence: “No change is saved twice.”

Here’s what came back:

NoChangeIsSavedTwice breaks. The shortest path has 4 steps:
1. you add or tick a todo
2. the server saves it, the answer gets lost
3. you press Retry
4. the server saves it and answers

This result convinced me. It reads like a bug report. I didn’t tell the checker where to look. It tried everything and gave me the shortest way to break my rule.

I gave it four rules. It visited all 729 states, and three of the rules broke.

Take the last one. Tick a todo right after you add it, and the tick can reach the server before the todo exists.

That’s three bugs in 19 lines I would have approved.

Each bug turned into a small design change.

The spinner bug comes from a boolean that several requests write to. So the boolean goes away. The status and the queue become one type:

// src/features/todos/save-queue.ts
type Sync =
  | { status: 'saved' }
  | { status: 'sending'; queue: Queue }
  | { status: 'failed'; queue: Queue }

That’s the state machine from the diagram, written as a type. “Saved with something still in the queue” doesn’t compile anymore.

The order bug comes from parallel requests. So changes wait in that queue, and only the first one is in flight.

The duplicate comes from a retry that looks new. So each change gets an id when you make it, and the server ignores an id it already applied:

// src/api/server.ts
export function receive(server: ServerState, mutation: Mutation): ServerState {
  if (server.applied.has(mutation.id)) return server
  // apply the change and remember its id
}

The id belongs to the change, not to the request. Create a new one per request and the dedupe does nothing.

I ran the checker again. It found 28 states instead of 729, and all five rules hold.

Writing the code as a state machine has one more benefit. The model and the code have the same states and the same events, so I can compare them line by line.

It also draws the whole thing, in the words a user would use:

I really like this chart. I can look at it and ask “is that how my app should behave?” without opening a file.

Look at where the three fixes went: a type, a queue behind one function and an id on the data.

None of them is a test.

That’s how I want it to work. Verification finds the bug, and the codebase makes it impossible. The next agent that changes my save logic can’t bring the spinner bug back. There’s no boolean to set.

It checks a design. It doesn’t check your code.

Remember the floor plan. Nothing forces it to match the house.

My model says the server ignores a repeat. If the real receive function doesn’t, the checker won’t notice. A green model with broken code is worse than no model.

So the model needs a second check, a test that runs the real functions against the same rules. That’s property-based testing, and it gets its own post.

Two more things you should know:

• It has bounds. My rules hold for three changes. I didn’t prove them for three thousand.
• Watch it fail once. I turned the dedupe off in the model to see the rule break. I wouldn’t trust a model I never saw fail. Agents are good at TLA+ syntax and much worse at matching your real code.

I didn’t do this by hand. I used two skills from pstack, the plugin where Lauren Tan packages her workflow for coding agents. I wrote about it in Learning from pstackLearning from pstack: Build Your Own Reliable Coding Agent StackThe written version of my TypeScript Meetup Munich talk. What pstack teaches about planning, implementation, review and verification, and how to give your own agent a verification skill that proves its work.claude-codeai-agentsagentic-workflowsOct 21, 2026.

/create-formal-verification-skill looks for the code where a bug costs the most and tests cover the least. It writes the model, and it has to show each rule failing on a broken variant before it’s done. Then it adds a skill to your repo, so the next agent can rerun the check.

/statechart runs the checker and makes the result readable. The four-step bug story and the chart in this post came out of it.

I think the name formal verification scares people off. It sounds like proofs and Greek letters. What I got was a four-step bug report about my retry button.

Use it where the order of events can cause a bug. That means retries, optimistic updates, offline sync or a checkout. Skip it for a contact form.

And you don’t have to learn TLA+. Write down two sentences that must stay true. Then let your agent check them in every order.

Have you found a bug this way? I’d love to hear about it.

If you want to go deeper, Learn TLA+ is the best free introduction, and Amazon’s paper shows what it catches at scale.