---
name: spec-generation
description: "TLA+ spec generation from a modeling brief. Use when: (1) turning code analysis findings into a TLA+ specification, (2) generating model checking and trace validation specs, (3) producing instrumentation mappings for trace collection."
---

Read `guide.md` for the full workflow methodology.