I implemented MessagePort in Servo back in 2019 — it was the hardest concurrency problem I'd encountered, because ports can be transferred between event loops while messages are still in flight. This weekend I finally got around to formalizing it in TLA+, with Claude helping with the typing. The interesting outcome: the abstract spec (following the HTML standard) is so simple that the refinement proof itself serves as the inductive invariant. No additional invariants needed. TLC found no bugs in the Servo implementation, though it did help me make explicit a sequencing assumption that was implicit in the code. Happy to answer questions about the TLA+ approach or the Servo implementation.