Skip to content

Add OCI use TLA+. #36

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
lemmy merged 1 commit into from
Sep 18, 2025
Merged

Add OCI use TLA+. #36

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions content/industry/index.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down