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

Beginne mit docs/design/ORCHESTRATOR.md und dem Zustandsdiagramm in ORCHESTRATOR.md und überprüfe anschließend die Abhängigkeit vom Refactoring der reinen Entscheidungsfunktion. Definiere das TLA+-Modell in formal/ oder docs/formal/, überprüfe die aufgeführten Invarianten mit TLC und dokumentiere die Zuordnung von TLA-Zuständen zu Code-Enums. Als erledigt gilt die Aufgabe, wenn das Modell und die Zuordnungen die Zustandsmaschine der Aufgabe abdecken und der vorgeschlagene CI-Weg zur Modellprüfung dokumentiert ist.

Vom Indexierungsmodell aus dem Issue-Text verfasst.