1. Overview
3. Tutorials
4. 1. Overview
5. 2. Entry-level Model Checker Tutorial
6. 3. Type Checker Tutorial
7. 4. Checking Pluscal specifications
8. 5. Apalache trail tips: how to check your specs faster
9. 6. Symbolic Model Checking
10. 7. Specifying temporal properties and understanding counterexamples
12. HOWTOs
13. 8. Overview
14. 9. How to write type annotations
15. 10. How to use uninterpreted types
17. Apalache User Manual
18. 11. Getting Started
    1. 11.1. Installation
       1. 11.1.1. Prebuilt Packages
       2. 11.1.2. Docker
       3. 11.1.3. Build from Source
    2. 11.2. Running the Tool
    3. 11.3. An Example TLA+ Specification
    4. 11.4. Specification Parameters
    5. 11.5. Symbolic Model Checking with Apalache
       1. 11.5.1. Assignments and symbolic transitions
       2. 11.5.2. Folding sets and sequences
       3. 11.5.3. Invariants: State, Action, Trace
       4. 11.5.4. Enumeration of counterexamples
       5. 11.5.5. The Apalache Module
       6. 11.5.6. Naturals
    6. 11.6. Apalache global configuration file
    7. 11.7. TLA+ Execution Statistics
    8. 11.8. Profiling Your Specification
    9. 11.9. Five minutes of theory
19. 12. Fine Tuning
20. 13. TLC Configuration Files
21. 14. The Snowcat Type Checker
22. 15. Supported Features
23. 16. Obsolete: Recursive operators and functions
24. 17. Known Issues
25. 18. Antipatterns
26. 19. TLA+ Preprocessing
27. 20. Assignments and Symbolic Transitions in Depth
28. 21. KerA: kernel logic of actions
30. TLA+ Language Manual for Engineers
31. 22. Introduction
32. 23. The standard operators of TLA+
    1. 23.1. Booleans
    2. 23.2. Control And Nondeterminism
    3. 23.3. Conditionals
    4. 23.4. Integers
    5. 23.5. Sets
    6. 23.6. Logic
    7. 23.7. Functions
    8. 23.8. Records
    9. 23.9. Tuples
    10. 23.10. Sequences
    11. 23.11. Bags
33. 24. Apalache extensions
    1. 24.1. Apalache module
    2. 24.2. Variants
    3. 24.3. Option types
34. 25. User-defined operators
    1. 25.1. Top-level operator definitions
    2. 25.2. LET-IN definitions
    3. 25.3. Higher-order operators definitions
    4. 25.4. Anonymous operator definitions
    5. 25.5. Local operator definitions
35. 26. Modules, Extends, and Instances
37. Idiomatic TLA+
38. 27. Introduction
39. 28. Keep state variables to the minimum
40. 29. Update state variables with assignments
41. 30. Apply primes only to state variables
42. 31. Use Boolean operators in actions, not IF-THEN-ELSE
43. 32. Avoid sets of mixed records
45. Design Documents
46. 33. RFC 001: types and type annotations
47. 34. ADR-002: types and type annotations
48. 35. ADR-003: transition executor (TRex)
49. 36. ADR-004: code annotations
50. 37. ADR-005: JSON Serialization Format
51. 38. RFC-006: unit tests and property-based tests
52. 39. ADR-007: restructuring
53. 40. ADR-008: exceptions
54. 41. ADR-009: outputs
55. 42. RFC-010: Implementation of Transition Exploration Server
56. 43. ADR-011: alternative SMT encoding using arrays
57. 44. ADR-012: Adopt an ADR Template
58. 45. ADR-013: Configuration Management Component
59. 46. ADR-014: Precise type inference for records and variants
60. 47. ADR-015: ITF: informal trace format
61. 48. ADR-016: ReTLA: Relational TLA
62. 49. PDR-017: Checking temporal properties
63. 50. ADR-018: Inlining in Apalache
64. 51. ADR-019: Harmonize changelog management
65. 52. ADR-020: Improving membership in arenas
66. 53. RFC-021: Prioritization of Work
67. 54. ADR-022: Unify Configuration Management and "Pass Options"
68. 55. ADR-023: Trace evaluation
69. 56. ADR-024: Arena computation isolation
70. 57. ADR-025: CVC5 solver backend integration