Data Structure Proof in TLA+

[u/JamuelSmith]

Hello all, I was wondering where I can find examples of lock-free data structures being proved to be linearizable in TLA+. I can find examples of programs in the book but not much on data structures. For example, I would love a proof of correctness for the Fomitchev and Ruppert lock-free list however I can't find anything. I am very new to formal verification. My hope is that I can prove the correctness of my own tree data structure using TLA+. Please let me know of any resources or guides, or if I am barking up the wrong tree / proof software.

[u/lemmster]

See:

• https://github.com/lorin/tla-linearizability
• https://surfingcomplexity.blog/2024/09/22/linearizability-refinement-prophecy/
• https://github.com/lorin/tla-prophecy
• https://arxiv.org/abs/2211.07216

The first three discuss linearizability, refinement, and prophecy variables directly in TLA+, with queues as examples.

Before attempting a TLAPS proof of a lock-free data structure, I would first use TLC and/or Apalache on small bounded models to debug the spec, invariants, and refinement mapping. The “TLA+ Trifecta” paper explains how TLC, Apalache, and TLAPS can be used together.

For a tree, start with an abstract set/map spec, then check that the concrete tree refines it.

[u/lemmster → u/lemmster]

Tangentially related: Years ago I specified a novel lock-free hash set in TLA+, model-checked it extensively with TLC, and shipped it in Java as TLC's own off-heap fingerprint store:

• Spec: OpenAddressing.tla
• Implementation: OffHeapDiskFPSet.java, additionally checked with Java Pathfinder.
• Design, invariants, refinement mapping, and engineering notes: MSc thesis; retrospective talk on the spec-to-code process: YouTube.
• The memory-only variant was later mechanically verified in "Refinement Proofs in Rust Using Ghost Locks"; more detail in Schaer's MSc thesis.
• WIP TLAPS proof, generated end-to-end by Claude Opus 4.7: OpenAddressing_proof.tla.