On Monday, September 28, 2026 at 9:38:45 AM UTC-7 Markus Kuppe wrote:
One more for the list: TLC's DiskStateQueue, i.e. the disk-backed queue used by the model checker: https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/spec/queue/DiskStateQueue.tla
It resulted from this PR: https://github.com/tlaplus/tlaplus/pull/1446. The PR is interesting beyond this particular spec. Ordinary TLA+ trace validation checks traces from tests or production workloads against a spec. Here, Java Pathfinder (JPF) model-checked the Java implementation and fed the resulting executions to TLC for trace validation. This also made it possible to trace-validate executions involving spurious wakeups, which are very difficult to trigger with ordinary trace validation.
M.
> On Sep 9, 2026, at 1:35 PM, Chris Ortiz <zitro...@xxxxxxxxx> wrote:
>
> Thank you very much Markus. I will take a look at them. These will help me understand those tools better.
>
> Thanks, and best regards,
> Chris (zitro)
>
> On Wednesday, September 9, 2026 at 12:51:58 PM UTC-7 Markus Kuppe wrote:
> Hi Chris,
>
> TLC's model checking algorithm (BFS exploration + error-trace construction):
> * https://github.com/tlaplus/examples/blob/master/specifications/TLC/TLCMC.tla
> * https://github.com/tlaplus/examples/blob/master/specifications/TLC/MCReachability.tla
>
> TLC's off-heap fingerprint set (OffHeapDiskFPSet.java); an in-memory variant was
> re-verified independently in https://arxiv.org/abs/2311.14452:
> * https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tlc2/tool/fp/OpenAddressing.tla
> * https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tlc2/tool/fp/OpenAddressing.ConcurrentFlusher.tla
>
> TLC's filesystem caching layer, with a refinement proof:
> * https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tlc2/util/BufferedRandomAccessFile.tla
> * https://github.com/tlaplus/examples/blob/master/specifications/braf/BufferedRandomAccessFile.tla
>
> TLC's lazy enumeration order for SUBSET S:
> * https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tlc2/value/impl/SubsetValue.tla
>
> Multi-core on-the-fly SCC decomposition, the algorithm class behind parallel
> liveness checking:
> * https://github.com/tlaplus/tlaplus/blob/master/general/performance/Bloemen/BloemenSCC.tla
>
> SANY's level checking, i.e. Specifying Systems 17.2 and the reference comment in
> LevelNode.java:
> * https://github.com/tlaplus/examples/blob/master/specifications/LevelChecking/LevelSpec.tla
>
> The grammar of TLA+, and of TLC's .cfg files, both written in TLA+:
> * https://github.com/tlaplus/examples/blob/master/specifications/SpecifyingSystems/Syntax/TLAPlusGrammar.tla
> * https://github.com/tlaplus/examples/blob/master/specifications/SpecifyingSystems/TLC/ConfigFileGrammar.tla
>
> The PlusCal translation step, plus the PlusCal-to-TLA+ location mapping the
> Toolbox uses to jump between code and translation:
> * https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/pcal/PlusCal.tla
> * https://github.com/tlaplus/tlaplus/blob/master/general/docs/TLAToPCal.tla
> * https://github.com/tlaplus/tlaplus/blob/master/general/docs/RemoveRedundantParens.tla
>
> How the Toolbox colors proof steps from TLAPM's per-obligation statuses:
> * https://github.com/tlaplus/tlaplus/blob/master/general/docs/ProofStatus.tla
> * https://github.com/tlaplus/tlaplus/blob/master/general/docs/ColorPredicates.tla
>
> M.
>
> > On Sep 9, 2026, at 11:06 AM, Chris Ortiz <zitro...@xxxxxxxxx> wrote:
> >
> > Hi TLA+ Community,
> >
> > Good morning. I would like to know if there are TLA+ Specs of the TLA+ tool ecosystem out there that we can refer to? Kindly let me know where I can find them if they exist. If not, there should be no reason why we cannot demonstrate writing TLA+ spec for the specification of the software that helps evangalize TLA+.
> >
> > Thanks, and best regards,
> > Chris (zitro)