# Marc Brooker et al. - Systems Correctness Practices At Aws (Highlights) ![rw-book-cover|256](https://readwise-assets.s3.amazonaws.com/media/reader/parsed_document_assets/463450203/WbeFF4jhiwsFbwyuKod3ztUsmvLWh9ne1zyTodykRk8-cove_oT7Ailv.png) ## Metadata **Review**:: [readwise.io](https://readwise.io/bookreview/61107089) **Source**:: #from/readwise #from/reader **Zettel**:: #zettel/fleeting **Status**:: #x **Authors**:: [[Marc Brooker]], [[Ankush Desai]] **Full Title**:: Systems Correctness Practices At Aws **Category**:: #articles #readwise/articles **Category Icon**:: 📰 **Document Tags**:: #via/ddia **URL**:: [readwise.io](https://readwise.io/reader/document_raw_content/463450203) **Host**:: [[readwise.io]] **Highlighted**:: [[2026-06-12]] **Created**:: [[2026-06-13]] ## Note https://spawn-queue.acm.org/doi/pdf/10.1145/3712057 ## Highlights - lightweight semi-formal approaches such as property-based testing,6,19 fuzzing,9 and runtime monitoring.11 ([View Highlight](https://read.readwise.io/read/01ktwjfwt6sb45nec4pzk89xas)) ^1024489567 - P is a state-machine-based language for modeling and analysis of distributed systems. ([View Highlight](https://read.readwise.io/read/01ktwjh738wv5p8t8xcsrdqb5q)) ^1024489639 - With PObserve, we take structured logs from the execution of distributed systems and validate post-hoc that they match behaviors allowed by the formal P specification of the system. ([View Highlight](https://read.readwise.io/read/01ktwk0pfdasm0gqhsaqras08p)) ^1024490272 - Some of the work done at AWS on build-time testing of thread ordering and systems failures has been open-sourced as part of the shuttle (https://github.com/awslabs/shuttle) and turmoil (https://github.com/tokio-rs/turmoil) projects. ([View Highlight](https://read.readwise.io/read/01ktwk392vymvyp65hnwsbtns0)) ^1024490334 - Large volumes of random SQL schemas, datasets, and queries are synthesized and run through the engines under test, and the results compared with an oracle based on the nonsharded version of the engine (as well as other approaches to validation, like those pioneered by SQLancer23). ([View Highlight](https://read.readwise.io/read/01ktwk7jkba9cp7kh91h1v8w1z)) ^1024490566 - In early 2021 AWS launched FIS (Fault Injection Service)2 with the goal of making testing based on fault injection accessible to a wide range of AWS customers. ([View Highlight](https://read.readwise.io/read/01ktwk8wv21s8hsbfb1dvgd6jr)) ^1024490605