Open source tools for software engineering teams using AI
← Blog

Using Formal Methods on a Recurring Connection Bug

correctnessformal methods

We build small tools for coordinating and running AI agents. One of them, Biff, had a connection bug we could not kill.

Biff uses NATS as its message relay. NATS is an open-source messaging system [1]. It carries messages between agents on streams, and tracks who is online in key-value buckets. Biff’s connection to NATS failed the same way each time. The socket, the connection’s open endpoint, stayed open, but every request to the streams and buckets timed out, and the retry loop ran on a dead connection until the session locked up. We fixed it. It came back. Over several months we changed the connection code six times, and the same failure returned.

A test checks only the sequences of events it is written to check. A bug that survives six patches is living in a sequence nobody wrote a test for. Writing a seventh test is a guess. We tried something else. We described the connection in mathematics and had a tool check every sequence at once.

The model, before and after

Describing the connection in mathematics means writing a specification: an exact account of the states a system can be in and what must be true in each one. This is a long-standing engineering discipline called formal methods. A test checks the cases it runs. A specification lets a tool check every case, because the description is precise enough to reason about instead of execute.

We write ours in Z. Z is built on two pieces of mathematics. The first is set theory, the study of collections of things. The second is predicate logic, statements that are either true or false and the symbols that join them, such as ∧ for “and” and ⟹ for “implies”. They appear in the model below. Z was developed at Oxford and is an ISO standard [3]. A Z specification names the states a system can hold, the rules that constrain them, and the operations that move between them.

Z Spec is our Claude Code plugin for working with these specifications. code2model extracts a starting specification from existing code. model2code generates code from one [2]. This connection already had a specification, so we extended it by hand. z-spec check type-checks it and confirms it is internally consistent.

Our first model had three connection modes.

ConnState ::= disconnected | connected | closed

None of them was the failure. There was no mode for socket-open-but-not-connected. A model that cannot describe a failure cannot rule it out. So we named the two missing modes.

ConnState ::= disconnected | reconnecting | connected | halfOpen | closed

Here is the rule that ties a connection’s mode to the resources it holds.

Connection
  connState : ConnState
  kvProvisioned, streamsProvisioned, namesProvisioned : Bool
  ─────────────────────────────────────────────────────────────
  connState ≠ connected ⟹ kvProvisioned = false ∧ streamsProvisioned = false ∧ namesProvisioned = false
  connState = connected ⟹ kvProvisioned = true  ∧ streamsProvisioned = true  ∧ namesProvisioned = true

That block is a schema: one named piece of a specification. The lines above the divider declare the state, here the connection’s mode and three flags for the NATS resources it holds, the message streams and two key-value buckets. The lines below are an invariant, a rule that must hold in every state. This one says the resources are ready when the connection is connected, and at no other time. The new mode halfOpen is the bug: socket open, connection not connected, every request failing.

What ProB does with it

The next command, z-spec test, runs a checker called ProB [4]. ProB reads the specification and explores every state the system can reach. It reports any state that breaks an invariant, and any state the system can enter and never leave. To confirm our model caught the bug, we removed the one recovery step and ran z-spec test. It printed this.

*** COUNTER EXAMPLE FOUND ***
deadlock
*** TRACE (length=4):
 1: SETUP_CONSTANTS(...)
 2: INITIALISATION(connState=disconnected, kvProvisioned=false, ...)
 3: EnsureConnected(connState=connected, kvProvisioned=true, ...)
 4: Request-->reqTimeout
Found "deadlock" error in state id 4

The trace reads top to bottom. The connection starts disconnected. It connects. A request times out, which moves it to halfOpen. From halfOpen nothing is possible, so it is stuck. deadlock is ProB’s word for a state with no way out. State 4 is the production bug, reproduced from the model as a four-step trace.

With the recovery step back, the check passes.

z-spec test docs/nats-relay-passA-nowedge.tex   →  ok: false, deadlock
z-spec test docs/nats-relay.tex                 →  ok: true, 6 states, deadlock-free, all operations covered

The model demanded a way out of halfOpen, and the code now has two independent ones. One tunes the keepalive, the interval between the pings that keep a connection alive, so a dead connection shows up in about sixty to eighty seconds. The other is a reconnect that fires on its own after three failed requests, in about fifteen. The model proves that either one alone breaks the deadlock, so the connection can never stay stuck. The model is now what the code must satisfy, and we check connection changes against it before they merge.

Before, the connection had one slow way out and no fast one.

# ~240s to notice a dead connection
await nats.connect(..., ping_interval=120, max_outstanding_pings=2)
# a timed-out request just propagated; the poller and heartbeat
# retried the same dead connection, with no recovery

After, it has two.

# escape 1: tune the keepalive so a dead connection shows in ~60s
await nats.connect(..., ping_interval=20, max_outstanding_pings=3)

# escape 2: on a request timeout, count it; reconnect after three in a row
try:
    await self._js_or_kv_request(...)
except TimeoutError:
    self._health.record_timeout(op, is_connected=is_connected)   # count += 1
    if is_connected and self._health.should_force_reconnect(threshold=3):
        await self._force_reconnect()                            # ~15s, no wait
    raise

The keepalive escape is a configuration change. The proactive one counts timed-out requests and forces a reconnect at three. The model checks both against halfOpen, so a change to either is caught before it merges.

The model has to be able to fail

We wrote the model to fail before we wrote the fix, the way test-driven development starts from a failing test [10]. The difference is coverage: a test fails on one example, a model fails on every state that breaks a rule. So we hold the model to that bar. A specification proves nothing if it passes only because it is too vague to fail. We require that it reproduce the original bug when the fix is taken out. If it cannot, the model is too abstract to trust, and we make it more concrete until it can. Ours produced the four-step trace with the recovery step gone, and stopped once we put the step back.

The same spec is also a test plan

A model earns its cost twice. Two more Z Spec commands turn a specification into a test plan. partition derives the cases worth testing, one per meaningful boundary. audit maps those cases against the tests already written and lists the ones no test covers. On Lux, our display tool, the specification of how one display claims a screen slot produced this set of cases for a single operation.

P1   no socket file                     DEAD
P4   file present, no listener          DEAD
P5   bound, not yet accepting           DEAD   (the window)
P10  recycled pid file, no listener     DEAD   (identity from the socket, not the process id)

P5 is the bug that cost us sixteen rounds of fixes. A socket in the brief window after it is bound and before it accepts connections looks dead to a naive check, so a second process would claim the slot. The specification names that window as a case to test. A hand-written test suite rarely does.

Where this sits

Specification-driven development is a live trend. Most of it, in tools like Kiro, Spec Kit, and Tessl, starts from a specification written in natural language or lightly structured prose that an agent then implements [5, 6]. Our approach is older and narrower. We write the specification in Z, a mathematical notation, and have a tool check it rather than read it back. A related thread is arriving at the same place from formal verification, with growing interest in AI making proofs practical [7, 8], on top of a long history of formal methods in industry [9]. Proofs are a direction for us too. Z Spec can generate Lean proof obligations from a model, though the work here used model checking, not proof. None of this is ours to claim. We are trying it on small tools and reporting what we find.

What it cost, and what we do not yet know

Each model took an afternoon, because the agent drafts the notation and we correct it. That is the point. When a formal model costs hours instead of days, it becomes reasonable to reach for the second time a bug comes back.

The limits are real. These are small tools from a small team. We check each model for one or two processes, not for arbitrary numbers of them. We run the checks by hand and commit the results to the repository; they are not yet an automatic step in our build. The model did not replace our tests or our reviews. It sat next to them and caught the class of bug that sampling kept missing. We do not know how far this holds at larger scale. We are still finding out.

The specifications are public: Biff’s connection model is nats-relay.pdf, and Lux’s display model is display_lifecycle.pdf.

References

  1. Synadia. “NATS: Connective Technology for Adaptive Edge and Distributed Systems.” 2024. nats.io
  2. Punt Labs. “AI Coding + Grounding and Formal Methods = Agentic Software Engineering.” 2026. punt-labs.com
  3. ISO. “ISO/IEC 13568: Z Formal Specification Notation.” 2002. iso.org
  4. Leuschel, M. and Butler, M. “ProB: The Animator and Model Checker.” 2003. prob.hhu.de
  5. Fowler, M. “Understanding Spec-Driven Development: Kiro, spec-kit, and Tessl.” 2025. martinfowler.com
  6. Thoughtworks. “Spec-Driven Development.” Technology Radar, 2025. thoughtworks.com
  7. Kleppmann, M. “Prediction: AI Will Make Formal Verification Go Mainstream.” 2025. martin.kleppmann.com
  8. Councilman, A. et al. “Towards Formal Verification of LLM-Generated Code from Natural Language Prompts.” 2025. arxiv.org
  9. Newcombe, C. et al. “How Amazon Web Services Uses Formal Methods.” Communications of the ACM, 2015. cacm.acm.org
  10. Beck, K. “Test-Driven Development: By Example.” Addison-Wesley, 2002.