Re: [tlaplus] TLA+ Specs of TLA+ Tools like TLC, TLaTeX, etc.

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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 <zitroomega@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)


-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/919F5A6E-9594-42BE-AAF8-8510EAB23F63%40lemmster.de.