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

docs/design/ORCHESTRATOR.md と ORCHESTRATOR.md の状態図から始め、次に pure decision function のリファクタリング依存関係を確認します。formal/ または docs/formal/ に TLA+ モデルを定義し、列挙された不変条件を TLC で検証して、TLA の状態からコードの enum への対応関係を文書化します。モデルと対応関係がタスクの状態機械をカバーし、提案された CI によるモデル検査の手順が文書化されていれば完了です。