# Use of Formal Methods at Amazon Web Services

DevFeed: [Use of Formal Methods at Amazon Web Services](<https://devfeed.tech/articles/use-of-formal-methods-at-amazon-web-services-12461.md>)

Original publisher: [Read original article](<http://brooker.co.za/blog/2014/08/09/formal-methods.html>)

Author: Marc Brooker

Published: 2014-08-09T00: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>), [Amazon Web Services](<https://devfeed.tech/topics/aws.md>)

Tags: [amazon](<https://devfeed.tech/tags/amazon.md>), [amazon-web-services-aws](<https://devfeed.tech/tags/amazon-web-services-aws.md>), [code](<https://devfeed.tech/tags/code.md>), [concurrency](<https://devfeed.tech/tags/concurrency.md>), [formal-methods](<https://devfeed.tech/tags/formal-methods.md>)

## AI overview

The article describes how Amazon Web Services uses formal methods, particularly TLA+, to create precise system designs and detect subtle design errors. It explains that precise descriptions make assumptions about failures and concurrency explicit while avoiding the excessive detail of executable code.

## Source excerpt

Use of Formal Methods at Amazon Web Services How we're using TLA+ at AWS Late last year, we published Use of Formal Methods at Amazon Web Services about our experiences with using formal methods at Amazon Web Services (AWS). The focus is on TLA+, and why we think it's a great fit for the kind of work we do. From the paper: In order to find subtle bugs in a system design, it is necessary to have a precise description of that design. There are at least two major benefits to writing a precise design; the author is forced to think more clearly, which helps eliminate 'plausible hand-waving', and tools can be applied to check for errors in the design, even while it is being written. In contrast, conventional design documents consist of prose, static diagrams, and perhaps pseudo-code in an adhoc untestable language. Such descriptions are far from precise; they are often ambiguous, or omit critical aspects such as partial failure or the granularity of concurrency (i.e. which constructs are assumed to be atomic). At the other end of the spectrum, the final executable code is unambiguous, but contains an overwhelming amount of detail. We needed to be able to capture the essence of a design in a few hundred lines of precise description. The full paper is worth reading if you're interested in formal methods.