←back to thread

Systems Correctness Practices at AWS: Leveraging Formal and Semi-Formal Methods

(queue.acm.org)
167 points yarapavan | 1 comments | 01 Apr 25 14:59 UTC | HN request time: 0.223s | source
Show context
nullorempty ◴[01 Apr 25 16:08 UTC] No.43548459[source]▶
And what teams use these methods exactly?
replies(2): >>43548526 #>>43552340 #
riknos314 ◴[01 Apr 25 16:14 UTC] No.43548526[source]▶
The article directly mentions several.

> Teams across AWS that build some of its flagship products—from storage (e.g., Amazon S3, EBS), to databases (e.g., Amazon DynamoDB, MemoryDB, Aurora), to compute (e.g., EC2, IoT)—have been using P to reason about the correctness of their system designs.

Later it more specifically mentions these (I probably missed a few):

S3 index, S3 ShardStore, Firecracker VMM, Aurora DB engine commit protocol, The RSA implementation on Graviton2

(EDIT: formatting)

replies(1): >>43548652 #
1. yarapavan ◴[01 Apr 25 16:24 UTC] No.43548652[source]▶
If you are wondering "why do formal methods at all?" or "how is AWS using P to gain confidence in correctness of their services?", the following re:Invent 2023 talk answers this question, provides an overview of P, and its impact inside AWS: (Re:Invent 2023 Talk) Gain confidence in system correctness & resilience with Formal Methods (Finding Critical Bugs Early!!) - https://www.youtube.com/watch?v=FdXZXnkMDxs

Github: https://github.com/p-org/P