From 93f7d258f9767cec1285e1c1fc8cbced2ab5db44 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Thu, 18 Sep 2025 09:13:15 -0700 Subject: [PATCH] Add OCI use TLA+. Signed-off-by: Markus Alexander Kuppe --- content/industry/index.md | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/content/industry/index.md b/content/industry/index.md index dd74782..5d32f76 100644 --- a/content/industry/index.md +++ b/content/industry/index.md @@ -148,6 +148,15 @@ They have also employed TLA⁺ for model-based trace checking and for modular sp > > William Schultz, Murat Demirbas, VLDB 2025 +## Oracle + +Oracle Cloud Infrastructure (OCI) has been using TLA+ since 2015 to verify storage systems and critical low-level services. + +In 2022 OCI published a [blog post](https://blogs.oracle.com/cloud-infrastructure/post/sleeping-soundly-with-the-help-of-tla) about one specific use of TLA+ to verify a system that automates certain hard drive operations: + +> TLA+ has been a huge success. We have uncovered many subtle bugs like our example before they caused damage in production. The drive manager has also been a huge success: No data lost and thousands of operator hours saved. We believe this success is due in part to the extra time that we spent formalizing and verifying the design before deploying the system. + +Calvin Loncaric, a principal engineer at Oracle, also gave [a talk at TLA+ Conference 2024](https://conf.tlapl.us/2024/) about how OCI uses TLA+ to find bugs in existing systems with hundreds of thousands of lines of code, not just as an ahead-of-time design tool. The talk reveals that OCI has written hundreds of TLA+ specifications covering dozens of cloud services. ## OpenComRTOS