{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T20:16:52Z","timestamp":1784233012939,"version":"3.55.0"},"reference-count":25,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2024,12,31]],"date-time":"2024-12-31T00:00:00Z","timestamp":1735603200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Queue"],"published-print":{"date-parts":[[2024,12,31]]},"abstract":"<jats:p>Building reliable and secure software requires a range of approaches to reason about systems correctness. Alongside industry-standard testing methods (such as unit and integration testing), AWS has adopted model checking, fuzzing, property-based testing, fault-injection testing, deterministic simulation, event-based simulation, and runtime validation of execution traces. Formal methods have been an important part of the development process - perhaps most importantly, formal specifications as test oracles that provide the correct answers for many of AWS's testing practices. Correctness testing and formal methods remain key areas of investment at AWS, accelerated by the excellent returns seen on investments in these areas already.<\/jats:p>","DOI":"10.1145\/3712057","type":"journal-article","created":{"date-parts":[[2025,2,4]],"date-time":"2025-02-04T23:18:41Z","timestamp":1738711121000},"page":"79-96","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Systems Correctness Practices at AWS"],"prefix":"10.1145","volume":"22","author":[{"given":"Marc","family":"Brooker","sequence":"first","affiliation":[{"name":"Amazon Web Services"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ankush","family":"Desai","sequence":"additional","affiliation":[{"name":"Amazon Web Services"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,2,4]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Amazon S3 now delivers strong read-after-write consistency automatically for all applications","author":"Amazon Web Services 0.","year":"2020","unstructured":"Amazon Web Services. 2020. Amazon S3 now delivers strong read-after-write consistency automatically for all applications; https:\/\/aws.amazon.com\/about-aws\/whats-new\/2020\/12\/amazon-s3-now-delivers-strong-read-after-write-consistency-automatically-for-all-applications. (Announces automatic strong read-after-write consistency for all S3 operations across all AWS regions.)"},{"key":"e_1_2_1_2_1","volume-title":"Announcing general availability of AWS Fault Injection Simulator, a fully managed service to run controlled experiments","author":"Amazon Web Services","year":"2021","unstructured":"Amazon Web Services. 2021. Announcing general availability of AWS Fault Injection Simulator, a fully managed service to run controlled experiments; https:\/\/aws.amazon.com\/about-aws\/whats-new\/2021\/03\/aws-announces-service-aws-fault-injection-simulator\/."},{"key":"e_1_2_1_3_1","volume-title":"Announcing Amazon Aurora Limitless Database","author":"Amazon Web Services","year":"2023","unstructured":"Amazon Web Services. 2023. Announcing Amazon Aurora Limitless Database; https:\/\/aws.amazon.com\/about-aws\/whats-new\/2023\/11\/amazon-aurora-limitless-database\/."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477132.3483540"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3458336.3465286"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_2_1_7_1","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction ? CADE 28 (28th International Conference on Automated Deduction","author":"de Moura L.","unstructured":"de Moura, L., Ullrich, S. 2021. The Lean 4 theorem prover and programming language. In Automated Deduction ? CADE 28 (28th International Conference on Automated Deduction, volume 12699 of Lecture Notes in Computer Science, 625?635. Springer; https:\/\/dl.acm.org\/doi\/10.1007\/978-3-030-79876-5_37."},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Desai A. Gupta V. Jackson E. Qadeer S. Rajamani S. Zufferey D. 2013. P: safe asynchronous event-driven programming. ACM SIGPLAN Notices 48(6) 321?332; https:\/\/dl.acm.org\/doi\/10.1145\/2499370.2462184.","DOI":"10.1145\/2499370.2462184"},{"key":"e_1_2_1_9_1","volume-title":"14th Usenix Workshop on Offensive Technologies; https:\/\/www.usenix.org\/conference\/woot20\/presentation\/fioraldi.","author":"Fioraldi A.","year":"2020","unstructured":"Fioraldi, A., Maier, D., Ei\u00dffeldt, H., Heuse, M. 2020. AFL++: Combining incremental steps of fuzzing research. In 14th Usenix Workshop on Offensive Technologies; https:\/\/www.usenix.org\/conference\/woot20\/presentation\/fioraldi."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_4"},{"key":"e_1_2_1_11_1","volume-title":"18th International Conference, RV 2018","volume":"11237","author":"Havelund K.","year":"2019","unstructured":"Havelund, K., Rosu, G. 2019. Runtime verification ? 17 years later. In Runtime Verification, 18th International Conference, RV 2018, Limassol, Cyprus, ed., C. Colombo and M. Leucker, 3?17, volume 11237 of Lecture Notes in Computer Science. Springer; https:\/\/link.springer.com\/book\/10.1007\/978-3-030-03769-7."},{"key":"e_1_2_1_12_1","unstructured":"Hicks M. 2023. How we built Cedar with automated reasoning and differential testing. Amazon Science; https:\/\/www.amazon.science\/blog\/how-we-built-cedar-with-automated-reasoning-and-differential-testing."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.14778\/3430915.3430918"},{"key":"e_1_2_1_14_1","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport L.","year":"2002","unstructured":"Lamport, L. 2002. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Professional."},{"key":"e_1_2_1_15_1","doi-asserted-by":"crossref","unstructured":"Lamport L. 2015. Who builds a house without drawing blueprints? Communications of the ACM 58(4) 38?41; https:\/\/dl.acm.org\/doi\/10.1145\/2736348.","DOI":"10.1145\/2736348"},{"key":"e_1_2_1_16_1","unstructured":"Lean Prover Community. 2024. Lean 4. GitHub; https:\/\/github.com\/leanprover\/lean4."},{"key":"e_1_2_1_17_1","unstructured":"Lee J. Becker H. Harrison J. 2024. Formal verification makes RSA faster?and faster to deploy. Amazon Science; https:\/\/www.amazon.science\/blog\/formal-verification-makes-rsa-faster-and-faster-to-deploy."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.21105\/joss.01891"},{"key":"e_1_2_1_20_1","volume-title":"Amazon Web Services","author":"Monteiro F.","year":"2023","unstructured":"Monteiro, F., Roy, P. 2023. Using Kani to validate security boundaries in AWS Firecracker. Technical report, Amazon Web Services; https:\/\/model-checking.github.io\/kani-verifier-blog\/2023\/08\/31\/using-kani-to-validate-security-boundaries-in-aws-firecracker.html."},{"key":"e_1_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Newcombe C. Rath T. Zhang F. Munteanu B. Brooker M. Deardeuff M. 2015. How Amazon Web Services uses formal methods. Communications of the ACM 58(4) 66?73. https:\/\/dl.acm.org\/doi\/10.1145\/2699417.","DOI":"10.1145\/2699417"},{"key":"e_1_2_1_22_1","unstructured":"P Team. 2024. P: a programming language for formal specification of distributed systems. https:\/\/github.com\/p-org\/P. (Used extensively in AWS and Microsoft for formal verification of distributed systems.)"},{"key":"e_1_2_1_23_1","volume-title":"14th Usenix Symposium on Operating Systems Design and Implementation, Article 38","author":"Rigger M.","year":"2020","unstructured":"Rigger, M., Su, Z. 2020. Testing database engines via pivoted query synthesis. In 14th Usenix Symposium on Operating Systems Design and Implementation, Article 38, 667?682; https:\/\/dl.acm.org\/doi\/10.5555\/3488766.3488804."},{"key":"e_1_2_1_24_1","volume-title":"Trillions of formally verified authorizations a day! Splash keynote","author":"Rungta N.","year":"2024","unstructured":"Rungta, N. 2024. Trillions of formally verified authorizations a day! Splash keynote; https:\/\/2024.splashcon.org\/details\/splash-2024-keynotes\/3\/Trillions-of-Formally-Verified-Authorizations-a-day-."},{"key":"e_1_2_1_25_1","volume-title":"Diving deep on S3 consistency. All Things Distributed","author":"Vogels W.","year":"2021","unstructured":"Vogels, W. 2021. Diving deep on S3 consistency. All Things Distributed; https:\/\/www.allthingsdistributed.com\/2021\/04\/s3-strong-consistency.html. (Blog post describing the implementation of strong consistency in Amazon S3.)"}],"container-title":["Queue"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3712057","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3712057","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:18:10Z","timestamp":1750295890000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3712057"}},"subtitle":["Leveraging Formal and Semi-formal Methods"],"short-title":[],"issued":{"date-parts":[[2024,12,31]]},"references-count":25,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2024,12,31]]}},"alternative-id":["10.1145\/3712057"],"URL":"https:\/\/doi.org\/10.1145\/3712057","relation":{},"ISSN":["1542-7730","1542-7749"],"issn-type":[{"value":"1542-7730","type":"print"},{"value":"1542-7749","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,12,31]]},"assertion":[{"value":"2025-02-04","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}