TLA+ (Temporal Logic of Actions): Mathematical specification language for concurrent and distributed systems, invented by Leslie Lamport

PlusCal: Higher-level pseudo code language that compiles to TLA+, more approachable for firmware engineers

PlantUML: Tool for generating UML sequence diagrams, activity diagrams, and flowcharts from textual descriptions

LaTeX & LuaLaTeX: Document preparation system for high-quality typesetting and PDF generation

Rust (Preferred) or Python: Primary programming languages for implementation

VSCode Extensions: TLA+ extension, LaTeX Workshop, Rust-analyzer, PlantUML, Graphviz Interactive Preview

Supporting Tools: OpenJDK ≥11.0.6, MiKTeX ≥25.3, Adobe Acrobat Reader, Git & GitHub