# Getting into formal specification, and getting my team into it too

DevFeed: [Getting into formal specification, and getting my team into it too](<https://devfeed.tech/articles/getting-into-formal-specification-and-getting-my-team-into-it-too-12522.md>)

Original publisher: [Read original article](<http://brooker.co.za/blog/2022/07/29/getting-into-tla.html>)

Author: Marc Brooker

Published: 2022-07-29T00:00:00Z

Content type: article

Language: en

Sources: [Marc Brooker's Blog](<https://devfeed.tech/sources/marc-brooker-s-blog.md>), [Marc Brooker's Blog](<https://devfeed.tech/sources/marc-brooker-s-blog-2.md>)

Topics: [Math and Logic](<https://devfeed.tech/topics/math-and-logic.md>), [Finite-state machine](<https://devfeed.tech/topics/finite-state-machine.md>), [debugging](<https://devfeed.tech/topics/debugging.md>), [Replication](<https://devfeed.tech/topics/replication.md>), [Network](<https://devfeed.tech/topics/network.md>)

Tags: [code](<https://devfeed.tech/tags/code.md>), [debugging](<https://devfeed.tech/tags/debugging.md>), [network](<https://devfeed.tech/tags/network.md>), [replication](<https://devfeed.tech/tags/replication.md>), [software](<https://devfeed.tech/tags/software.md>), [tools](<https://devfeed.tech/tags/tools.md>)

## AI overview

The article explains how a software engineer adopted formal specification while working on Amazon EBS control-plane changes. After debugging complex anti-entropy code with frequent failures during network partitions and system changes, the team modeled state transitions explicitly and explored Alloy and Spin before adopting TLA+ for reasoning about convergence and replication correctness.

## Source excerpt

Getting into formal specification, and getting my team into it too Getting started is the hard part Sometimes I write long email replies to people at work asking me questions. Sometimes those emails seem like they could be useful to more than just the recipient. This is one of those emails: a reply to a software engineer asking me how they could adopt formal specification in their team, and how I got into it. Sometime around 2011 I was working on some major changes to the EBS control plane. We had this anti-entropy system, which had the job of converging the actual system state (e.g. the state of the volumes on the storage fleet, and clients on the EC2 fleet1) with the intended system state in the control plane (e.g. the customer requested that this volume is deleted). We had a mess of ad-hoc code that took four sources of state (two storage servers, one EC2 client, the control plane), applied a lot of logic, and tried to figure out the steps to take to converge the states. Lots and lots of code. Debugging it was hard, and bugs were frequent. Most painfully, I think, wasn't that the bugs were frequent. It's that they came in bursts. The code would behave for months, then there would be a network partition, or a change in another system, and loads of weird stuff would happen all at once. Then we'd try to fix something, and it'd just break in another way. So we all took a day and drew up a huge state table on this big whiteboard in the hall, and circles and arrows showing the state transitions we wanted. A day well spent: we simplified the code significantly, and whacked a lot of bugs. But I wanted to do better. Specifically, I wanted to be able to know whether this mess of circles and arrows would always converge the state. I went looking for tools, and found and used Alloy for a while. Then Marc Levy introduced me to Spin, which I used for a while but never became particularly comfortable with. The next year we were trying to reason through some changes to replicati