An anecdotal example of the use of TLA+ The service I worked for in AWS had to built a key service, about 18 months-ish after launch. If the service got anyth

An anecdotal example of the use of TLA+ The service I worked for in AWS had to built a key service, about 18 months-ish after launch. If the service got anything wrong, it would wipe out the customer's data. Evaluating the conditions and making the right decisions wasn't that complicated, but it was complicated enough as it involved multiple service components to meet certain scaling properties. The need to not do the wrong thing was crucial, and so the decision was made to use TLA+ to make sure things were correct. Two senior engineers had designed the overall process and it had been through architectural review (so almost all the senior engineers in the team had seen and reviewed it, and in this case I know at least one well respected principal engineer had been involved. Potential problems had been identified and resolved). Everyone felt confident, but we wanted to be sure. The engineers spent about a week getting up to speed with TLA+, and then started writing up the formal proof of the process, defining the valid states etc. before letting the model checker at it. Problems were found. A number of them, in fact, mostly things that are hard to just mentally reason about that come with the increased complexity of the service being made from multiple parts that would need to communicate. A number of the bugs were of the type that would be unlikely to get exposed by any kind of unit/integration/functional testing. This is where the strong value proposition is for the use of TLA+, catching logical issues that are hard to reason about or test for, and Amazon has been using it to increasing amounts across services. The engineers involved, settled in to a refine/re-run cycle until they had eliminated the bugs. A final review was done of the TLA+ model and everyone was happy. After that they settled in to implementation phase, and they found that the way the model had ended up, it was relatively quick and simple to implement in Java. The model pretty much outlined everything that was needed in code. It became almost "fill in the blanks" coding, and there was a lot less mental effort involved for all in this stage. The initial optimistic estimate for the project was around 6 months, with extensive allowance for "shadow mode" running and verifying. The reality was that even with the time taken to learn, it was around 4 months from start to end, even including the time for engineers to learn TLA+ from scratch, and the service was launched with a high degree of confidence. The trick is that from here, you really need to think about keeping the model up to date. It should be seen as being as important as any other tests you've written for your actual code.