# Behavioral specification brief
State variables:
Initial condition:
Allowed actions:
Concurrency and failure assumptions:
Safety invariants:
Liveness requirements and fairness assumptions:
Model-checking bounds or proof obligations:
Observed result and counterexample trace:
Abstractions not covered:

## Review checklist
- [ ] Does the model retain relevant interleavings?
- [ ] Are checking bounds and assumptions recorded?
- [ ] Is a tool result distinguished from a handwritten trace?

Original template: Anuj Sadani, CC BY 4.0
Source guide: https://tech.anujsadani.in/ai-output-field-guide/approaches/tla-plus/