@@ -161,6 +161,7 @@ Jepsen is used by [CockroachDB](#cockroachlabs-cockroachdb), [VoltDB](#voltdb),
161161 using formal verification to find a bug in TimSort sorting algorithm
162162* [ Proving JDK’s Dual Pivot Quicksort Correct] ( https://www.key-project.org/2017/08/17/dual-pivot/ ) — analyzing quicksort
163163 implementation in Java
164+ * [ Formal Modeling and Analysis of Distributed Systems] ( https://youtu.be/5YjsSDDWFDY ) by Ankush Desai
164165
165166#### TLA+
166167
@@ -201,7 +202,7 @@ more popularity in recent years.
201202* [ What if we embraced simulation-driven development?] ( https://pierrezemb.fr/posts/simulation-driven-development/ ) by
202203 Pierre Zemb
203204* [ Deterministic simulation testing - how it works and when to use it] ( https://antithesis.com/resources/deterministic_simulation_testing/ ) —
204- overview of deterministic simulation testing by Antithesis.
205+ overview of deterministic simulation testing by Antithesis.
205206
206207More companies and systems adopt deterministic simulation as a primary testing strategy:
207208
@@ -385,6 +386,8 @@ specifically regression testing for correctness and performance bugs.
385386 testing and stateless model checking extensively to balance trade-offs and follow pragmatic approach.
386387 I gave a talk [ "Formal Methods at Amazon S3"] ( https://asatarin.github.io/talks/2022-02-formal-methods-at-amazon-s3/ )
387388 on this paper for a reading group.
389+ * [ Gain confidence in system correctness & resilience with formal methods] ( https://youtu.be/FdXZXnkMDxs ) by Ankush Desai
390+ * [ Fifteen years of formal methods at AWS] ( https://youtu.be/HxP4wi4DhA0 ) by Marc Brooker
388391
389392See also [ formal methods] ( #formal-methods ) and [ deterministic simulation] ( #deterministic-simulation ) sections.
390393
@@ -420,6 +423,7 @@ See also [chaos engineering](#chaos-engineering) and [lineage-driven fault injec
420423* [ Inside Azure Search: Chaos Engineering] ( https://azure.microsoft.com/en-us/blog/inside-azure-search-chaos-engineering/ )
421424* [ TLA+ at Microsoft: 16 Years in Production] ( https://youtu.be/azx6cX-BlCs ) by David Langworthy — how rejuvenation of
422425 TLA+ happened at Microsoft in 2016 and onwards
426+ * [ Formal Methods at Microsoft] ( https://youtu.be/GEsvGGp0jyQ ) by Nikolaj Bjørner
423427
424428See also [ formal methods] ( #formal-methods ) section.
425429
@@ -706,7 +710,8 @@ There is also talk from Sean T. Allen on testing stream processing system at Wal
706710* [ Verifying Transactional Consistency with Jepsen] ( https://medium.com/fauna/verifying-transactional-consistency-with-jepsen-and-faunadb-561eddd123c7 ) —
707711 results of internal [ Jepsen] ( #jepsen ) testing at FaunaDB
708712* [ Jepsen: FaunaDB 2.5.4] ( https://jepsen.io/analyses/faunadb-2.5.4 ) — official [ Jepsen] ( #jepsen ) test for FaunaDB,
709- write-up in Fauna [ blog] ( https://web.archive.org/web/20250516064357/https://fauna.com/blog/faunadbs-official-jepsen-results )
713+ write-up in
714+ Fauna [ blog] ( https://web.archive.org/web/20250516064357/https://fauna.com/blog/faunadbs-official-jepsen-results )
710715
711716### Shopify
712717
0 commit comments