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)