From 515649d1d55cf4fa7a2923209f50f610b53d62c0 Mon Sep 17 00:00:00 2001 From: Andrey Satarin Date: Sat, 29 Apr 2023 09:22:47 -0700 Subject: [PATCH] Add more internal links about formal methods --- README.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/README.md b/README.md index 5f1e9f3..48c26cd 100644 --- a/README.md +++ b/README.md @@ -109,7 +109,9 @@ Jepsen is used by [CockroachDB](#cockroachlabs-cockroachdb), [VoltDB](#voltdb), Companies using TLA+ to verify correctness of algorithms: * [Amazon Web Services](#amazon-web-services) * [PingCap for TiDB](#pingcap-tidb) + * [Elastic](#elastic-elasticsearch) * [MongoDB](#mongodb) + * [CockroachLabs](#cockroachlabs-cockroachdb) * [Microsoft](#microsoft) for services in Azure cloud * [Confluent](#confluent-kafka) for Apache Kafka @@ -315,6 +317,8 @@ Great discussion on tradeoffs between determinism, strengh of test oracles vs wi * [Growing a protocol](https://blog.acolyer.org/2017/08/23/growing-a-protocol/) — applying [lineage driven fault injection](#lineage-driven-fault-injection) to test Elasticsearch replication protocol * [Using TLA+ for fun and profit in the development of Elasticsearch](https://youtu.be/qYDcbcOVurc) by Yannick Welsch — Elasticsearch uses [TLA+](#formal-methods) to verify correctnes of their replication protocol +See also [formal methods](#formal-methods) section. + ### MongoDB * [MongoDB’s JavaScript Fuzzer: Creating Chaos (1/2)](https://www.mongodb.com/blog/post/mongodbs-java-script-fuzzer-creating-chaos)