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

Comienza con docs/design/ORCHESTRATOR.md y el diagrama de estados de ORCHESTRATOR.md; después, revisa la dependencia del refactor de la función de decisión pura. Define el modelo TLA+ en formal/ o docs/formal/, comprueba las invariantes indicadas con TLC y documenta la correspondencia entre los estados de TLA y los enums del código. Se considera completado cuando el modelo y las correspondencias cubren la máquina de estados de la tarea y queda documentado el flujo propuesto de CI para la comprobación del modelo.

Escrito por el modelo de indexación a partir del texto del issue.