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

Inizia da docs/design/ORCHESTRATOR.md e dal diagramma degli stati di ORCHESTRATOR.md, quindi esamina la dipendenza dal refactoring della funzione decisionale pura. Definisci il modello TLA+ in formal/ o docs/formal/, verifica gli invarianti elencati con TLC e documenta la corrispondenza tra gli stati TLA e gli enum del codice. L’attività è completata quando il modello e le corrispondenze coprono la macchina a stati dell’attività e il percorso proposto di model checking tramite CI è documentato.

Scritto dal modello di indicizzazione a partire dal testo della issue.