{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:08:27Z","timestamp":1776305307877,"version":"3.50.1"},"reference-count":25,"publisher":"Association for Computing Machinery (ACM)","license":[{"start":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T00:00:00Z","timestamp":1748476800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Commun. ACM"],"abstract":"<jats:p>Leveraging formal and semi-formal methods.<\/jats:p>","DOI":"10.1145\/3729175","type":"journal-article","created":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T13:29:21Z","timestamp":1748525361000},"update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Systems Correctness Practices at Amazon Web Services"],"prefix":"10.1145","author":[{"given":"Marc","family":"Brooker","sequence":"first","affiliation":[{"name":"Amazon Web Services, Seattle, WA, USA"}]},{"given":"Ankush","family":"Desai","sequence":"additional","affiliation":[{"name":"Amazon Web Services, Seattle, WA, USA"}]}],"member":"320","published-online":{"date-parts":[[2025,5,29]]},"reference":[{"key":"e_1_3_1_2_2","unstructured":"Amazon S3 now delivers strong read-after-write consistency automatically for all applications. Amazon Web Services (2020); https:\/\/tinyurl.com\/25mwxugm."},{"key":"e_1_3_1_3_2","unstructured":"Announcing general availability of AWS Fault Injection Simulator a fully managed service to run controlled experiments. Amazon Web Services (2021); https:\/\/tinyurl.com\/yhnr9nuj."},{"key":"e_1_3_1_4_2","unstructured":"Announcing Amazon Aurora Limitless Database. Amazon Web Services (2023); https:\/\/tinyurl.com\/28hwdrm8."},{"key":"e_1_3_1_5_2","doi-asserted-by":"crossref","unstructured":"Bornholt J. et al. Using lightweight formal methods to validate a key-value storage node in Amazon S3. In Proceedings of the ACM SIGOPS 28th Symp. Operating Systems Principles (2021) 836\u2013850; https:\/\/tinyurl.com\/2yczbl4s.","DOI":"10.1145\/3477132.3483540"},{"key":"e_1_3_1_6_2","doi-asserted-by":"crossref","unstructured":"Bronson N. Aghayev A. Charapko A. and Zhu T. Metastable failures in distributed systems. In Proceedings of the Workshop on Hot Topics in Operating Systems (2021) 221\u2013227; https:\/\/tinyurl.com\/2cqouvlf.","DOI":"10.1145\/3458336.3465286"},{"key":"e_1_3_1_7_2","doi-asserted-by":"crossref","unstructured":"Claessen K. and Hughes J. QuickCheck: A lightweight tool for random testing of Haskell programs. In Proceedings of the 5th ACM SIGPLAN Intern. Conf. Functional Programming (2000) 268\u2013279; https:\/\/tinyurl.com\/22jtuvwg.","DOI":"10.1145\/357766.351266"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/2499370.2462184"},{"key":"e_1_3_1_10_2","volume-title":"Proceedings of the 14th Usenix Workshop on Offensive Technologies","author":"Fioraldi A.","year":"2020","unstructured":"Fioraldi, A., Maier, D., Ei\u00dffeldt, H., and Heuse, M. 2020. AFL++: Combining incremental steps of fuzzing research. In Proceedings of the 14th Usenix Workshop on Offensive Technologies Usenix (2020); https:\/\/tinyurl.com\/27bwujn5."},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_4"},{"key":"e_1_3_1_12_2","volume-title":"Proceedings of the 18th Intern. Conf. ed.","author":"Havelund K.","year":"2019","unstructured":"Havelund, K. and Rosu, G. Runtime verification\u201417 years later. In Proceedings of the 18th Intern. Conf. ed., C. Colombo and M. Leucker 3\u201317, volume 11237 of Lecture Notes in Computer Science. Springer (2019); https:\/\/tinyurl.com\/2dnmzw9a."},{"key":"e_1_3_1_13_2","unstructured":"Hicks M. How we built Cedar with automated reasoning and differential testing. Amazon Science (2023); https:\/\/www.amazon.science\/blog\/how-we-built-cedar-with-automated-reasoning-and-differential-testing."},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.14778\/3430915.3430918"},{"key":"e_1_3_1_15_2","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport L.","year":"2002","unstructured":"Lamport, L. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Professional (2002)."},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/2736348"},{"key":"e_1_3_1_17_2","volume-title":"Lean 4","year":"2024","unstructured":"Lean Prover Community. Lean 4. GitHub (2024); https:\/\/tinyurl.com\/2yyzdba9."},{"key":"e_1_3_1_18_2","unstructured":"Lee J. Becker H. and Harrison J. Formal verification makes RSA faster\u2014and faster to deploy. Amazon Science (2024); https:\/\/www.amazon.science\/blog\/formal-verification-makes-rsa-faster-and-faster-to-deploy."},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.21105\/joss.01891"},{"key":"e_1_3_1_21_2","volume-title":"Technical report","author":"Monteiro F.","year":"2023","unstructured":"Monteiro, F. and Roy, P. Using Kani to validate security boundaries in AWS Firecracker. Technical report, Amazon Web Services (2023); https:\/\/tinyurl.com\/2cf6dub8."},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/2699417"},{"key":"e_1_3_1_23_2","unstructured":"P Team. P: A programming language for formal specification of distributed systems (2024); https:\/\/github.com\/p-org\/P"},{"key":"e_1_3_1_24_2","first-page":"667","article-title":"Testing database engines via pivoted query synthesis","volume":"38","author":"Rigger M.","year":"2020","unstructured":"Rigger, M. and Su, Z. 2020. Testing database engines via pivoted query synthesis. In Proceedings of the 14th Usenix Symp. on Operating Systems Design and Implementation, Article 38 (2020), 667\u2013682; https:\/\/tinyurl.com\/2da6rn2e.","journal-title":"Proceedings of the 14th Usenix Symp. on Operating Systems Design and Implementation, Article"},{"key":"e_1_3_1_25_2","doi-asserted-by":"crossref","unstructured":"Rungta N. Trillions of formally verified authorizations a day! Splash keynote (2024); https:\/\/tinyurl.com\/24ufvhff.","DOI":"10.1145\/3689491.3700409"},{"key":"e_1_3_1_26_2","unstructured":"Vogels W. Diving deep on S3 consistency. All Things Distributed; https:\/\/tinyurl.com\/2xo4xelw."}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729175","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729175","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:18:48Z","timestamp":1750295928000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729175"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,5,29]]},"references-count":25,"alternative-id":["10.1145\/3729175"],"URL":"https:\/\/doi.org\/10.1145\/3729175","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"value":"0001-0782","type":"print"},{"value":"1557-7317","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,5,29]]},"assertion":[{"value":"2025-05-29","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}],"article-number":"3729175"}}