verify: trace validation for the Coordinator model #266

The Coordinator TLA+ model (system shutdown) is checked by TLC only: the code records no coordinator events, so nothing ties the model to the implementation. It is allowlisted in verification/model-map.toml (#260) with this issue as its tracking item.

To close:

• emit coordinator lifecycle events from concurrency/src/system.rs (group shutdown order, grace and kill phases, helper drain);
• add a trace spec mapping them to Coordinator.tla actions, with invalid-trace controls;
• record traces from the shutdown tests and add them to trace_check.py;
• remove the allowlist entry and set a coverage floor.

Rule: models must be tied to the code through trace validation (ROADMAP, Verification rule).