Andrew Helwer<p>Reading the new experience report paper "System Correctness Practices at AWS" by <span class="h-card" translate="no"><a href="https://fediscience.org/@marcbrooker" class="u-url mention" rel="nofollow noopener" target="_blank">@<span>marcbrooker</span></a></span> & Ankush Desai, a successor to 2015 paper "How Amazon Web Services Uses Formal Methods". Documents a whole buffet of industrial formal methods use: P (including new tool PObserve for runtime trace validation), deterministic simulation testing in Rust with the open-sourced Shuttle and Turmoil tools, Dafny, HOL Light, and the open-sourced Kani model-checker for Rust.</p><p>While TLA⁺ was the most prominent featured tool in the 2015 paper, it's been lost in the crowd here as part of a clear shift toward verifying & testing the actual running code. I think TLA⁺ must carve out a niche for itself in a world where deterministic simulation testing becomes a commodity technology, or it risks losing relevance same as other design-level tools like UML. There are existing case studies on using TLA⁺ for trace validation and model-driven testing, but a lot of effort needs to go into tooling for making such integrations as smooth as possible instead of bespoke one-off projects.</p><p><a href="https://dl.acm.org/doi/10.1145/3712057" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">dl.acm.org/doi/10.1145/3712057</span><span class="invisible"></span></a></p><p><a href="https://discuss.systems/tags/TLAplus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>TLAplus</span></a> <a href="https://discuss.systems/tags/FormalMethods" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FormalMethods</span></a></p>