# Formal Methods Only Solve Half My Problems

DevFeed: [Formal Methods Only Solve Half My Problems](<https://devfeed.tech/articles/formal-methods-only-solve-half-my-problems-12520.md>)

Original publisher: [Read original article](<http://brooker.co.za/blog/2022/06/02/formal.html>)

Author: Marc Brooker

Published: 2022-06-02T00: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: [Formal methods](<https://devfeed.tech/topics/formal-methods.md>), [distributed-systems](<https://devfeed.tech/topics/distributed-systems.md>), [benchmarking](<https://devfeed.tech/topics/benchmarking.md>), [Protocol (disambiguation)](<https://devfeed.tech/topics/protocol.md>), [Latency](<https://devfeed.tech/topics/latency.md>), [Availability](<https://devfeed.tech/topics/availability.md>), [Hardware](<https://devfeed.tech/topics/hardware.md>), [Simulation and Design](<https://devfeed.tech/topics/simulation-and-design.md>)

Tags: [availability](<https://devfeed.tech/tags/availability.md>), [benchmarking](<https://devfeed.tech/tags/benchmarking.md>), [complexity](<https://devfeed.tech/tags/complexity.md>), [cost](<https://devfeed.tech/tags/cost.md>), [design](<https://devfeed.tech/tags/design.md>), [distributed-systems](<https://devfeed.tech/tags/distributed-systems.md>), [formal-methods](<https://devfeed.tech/tags/formal-methods.md>), [hardware](<https://devfeed.tech/tags/hardware.md>), [latency](<https://devfeed.tech/tags/latency.md>), [modelling](<https://devfeed.tech/tags/modelling.md>), [network](<https://devfeed.tech/tags/network.md>), [prototypes](<https://devfeed.tech/tags/prototypes.md>), [scale](<https://devfeed.tech/tags/scale.md>), [simulation](<https://devfeed.tech/tags/simulation.md>), [verification](<https://devfeed.tech/tags/verification.md>)

## AI overview

The article argues that formal methods such as TLA+ and P are highly valuable for finding bugs, exploring designs, and documenting protocols in large-scale distributed systems, but they address only part of the questions engineers face. It presents prototyping, closed-form modelling, benchmarking, and simulation as complementary techniques for evaluating latency, cost, hardware needs, availability, durability, overload behavior, and sensitivity to network conditions.

## Source excerpt

Formal Methods Only Solve Half My Problems At most half my problems. I have a lot of problems. The following is a one-page summary I wrote as a submission to HPTS'22. Hopefully it's of broader interest. Formal methods, like TLA+ and P, have proven to be extremely valuable to the builders of large scale distributed systems1, and to researchers working on distributed protocols. In industry, these tools typically aren't used for full verification. Instead, effort is focused on interactions and protocols that engineers expect to be particularly tricky or error-prone. Formal specifications play multiple roles in this setting, from bug finding in final designs, to accelerating exploration of the design space, to serving as precise documentation of the implemented protocol. Typically, verification or model checking of these specifications is focused on safety and liveness. This makes sense: safety violations cause issues like data corruption and loss which are correctly considered to be among the most serious issues with distributed systems. But safety and liveness are only a small part of a larger overall picture. Many of the questions that designers face can't be adequately tackled with these methods, because they lie outside the realm of safety, liveness, and related properties. What latency can customers expect, on average and in outlier cases? What will it cost us to run this service? How do those costs scale with different usage patterns, and dimensions of load (data size, throughput, transaction rates, etc)? What type of hardware do we need for this service, and how much? How sensitive is the design to network latency or packet loss? How do availability and durability scale with the number of replicas? How will the system behave under overload? We address these questions with prototyping, closed-form modelling, and with simulation. Prototyping, and benchmarking those prototypes, is clearly valuable but too expensive and slow to be used at the exploration stage. Deve