TLA+ / PlusCal track

This course is design-first and failure-first. TLA+ (and optionally PlusCal) is a tool for making assumptions explicit and checking whether a protocol sketch actually enforces the properties you claim.

Goal: use a small model to rule out bad designs early and to produce evidence-bearing artifacts for peer feedback and capstone risk reduction.

What this is (and is not)

• Is: a structured way to practice “invariants first” and to get concrete counterexamples (TLC traces) when an idea is wrong.
• Is not: a formal methods course; we keep models intentionally small and focused on one safety property at a time.

Where it appears in the term

• Week 03: first tiny model (atomic commit / coordination) + how to read a counterexample trace.
• Week 07–08: optional extension tied to DP2 (Paxos safety in a deliberately small model).
• Capstone: optional modeling milestone to de-risk assumptions and sharpen the failure evaluation plan.

Minimum expected artifacts

• One-page spec: state the failure model, the safety invariant(s), and the liveness assumption(s) you rely on.
• Model: a small TLA+ or PlusCal spec that captures just enough structure to check the invariant.
• Evidence: a TLC run (or equivalent) and either (a) “passes with invariant X” or (b) a counterexample trace plus your fix.
• Reflection: a short note explaining what the model changed about your design thinking.

How to use GenAI with TLA+ without fooling yourself

• Use GenAI for syntax and patterns (operators, state variables, typical spec structure).
• Use TLC as the judge: treat the model checker’s trace as the ground truth, not plausibility.
• Log decisions: record what you asked, what you adopted, and the TLC evidence that resulted.
• Explain in your own words: restate invariants and traces without copying tool output verbatim.

Recommended learning resource

• https://learntla.com/ (TLA+ fundamentals; PlusCal optional)