Verifying the Alternating Bit Protocol in Mathematica

Imagine two people passing notes across a classroom through unreliable messengers. The sender writes a message, tags it with a 0 or 1, and hands it off. The messenger might drop it. If the sender doesn’t hear back, they try again. When the receiver gets a new message, they send an acknowledgement – which might also get dropped. Despite all this unreliability, every message eventually arrives, exactly once, in order. One solution to this challenge is the algorithm called the Alternating Bit Protocol (ABP), Proving that the ABP works – that this complex network of retries and drops behaves identically to a simple reliable buffer – is a benchmark problem in formal verification, first established by Milner in CCS and revisited by dozens of researchers since.

We built a tool that carries out this proof mechanically for a finite-state instance of ABP (with 1-capacity lossy channels), in around 2,100 lines of Mathematica. The codebase, RCA, implements CCS with value-passing: processes communicate by synchronising on named channels, optionally exchanging data. The core is a transition function that computes every possible next step of a process expression — parallel composition with synchronisation, channel restriction, nondeterministic choice, and recursive definitions via a lightweight equation registry. On top of this sits a weak bisimulation game: a two-phase algorithm that explores the paired state space of two processes and determines whether they are observationally equivalent up to internal steps. For the 1-capacity ABP vs. a one-place buffer, the game explores 112 pairs across 114 reachable states and confirms the equivalence. The tool also provides strong bisimulation checking, symbolic transitions with constraints, and an interactive simulator with fold-back display of named agents.

For context, the Edinburgh Concurrency Workbench (CWB), the standard reference tool for this kind of analysis, was built by Cleaveland, Parrow, and Steffen at Edinburgh LFCS over 1987–1989, with Perdita Stevens later maintaining and extending the Edinburgh version from the mid-1990s. The CWB-NC successor comprises roughly 18,000 lines of Standard ML. RCA covers a meaningful fragment of the same ground in an order of magnitude less code — partly because Mathematica’s pattern-matching and symbolic rewriting are a natural fit for process algebra (CCS transition rules map almost directly to rewrite rules), and partly because the development was a close collaboration between a researcher with background in process calculus and Claude Opus 4.6, Anthropic’s AI coding agent. The human brought domain knowledge, design taste, and experienced testing; the AI contributed rapid implementation, bug diagnosis, and the ability to hold the full codebase in context while iterating. Neither could have done it alone at this pace.

~2,100 lines of code, ~20 commits, ABP verified. Happy to adjust tone, length, or emphasis.