TLA+ / Formal Verification

When and how to use TLA+ for design verification. Complements PBT (which verifies implementation).

Decision Tree: When to Use TLA+ vs PBT vs Both