chore: TLA+ formal verification of task state machine

**Context:** ROADMAP.md → Formal verification

---

## Component

Other

## Describe the feature

**TLA+ specification** of the task state machine, concurrency admission, cancellation races, and reconciler interleavings. Optional CI model checking on critical invariants.

## Use case

Subtle races (failTask double-emit #55, admission cap #331) are hard to catch with unit tests alone. Formal methods increase confidence as the state machine grows (PR watcher, queue states).

## Proposed solution

1. TLA+ model in `formal/` or `docs/formal/` mirroring `ORCHESTRATOR.md` state diagram.
2. Invariants: at-most-once terminal emit, concurrency counter consistency, no illegal transitions.
3. TLC model check in CI (nightly or on orchestrator diff).
4. Document mapping from TLA states to code enums.
5. Update when autonomous feedback loop adds states.

## Other information

- Depends on **pure decision function** refactor for tractable model.
- Design context: `docs/design/ORCHESTRATOR.md`.

- [ ] This might be a breaking change

Start with docs/design/ORCHESTRATOR.md and the ORCHESTRATOR.md state diagram, then review the pure decision function refactor dependency. Define the TLA+ model in formal/ or docs/formal/, check the listed invariants with TLC, and document the mapping from TLA states to code enums. Done means the model and mappings cover the task state machine and the proposed CI model-checking path is documented.

Written by the indexing model from the issue text.