"Running leading LLMs across the eleven systems shows that LLMs are great at producing correct TLA+ syntax but struggle to ensure conformance and appropriate invariants."

Slow stepping is a surprise; there's no OS reason for that to be slower. Possibly if your types are really large and complicated, the debugger has to fetch a lot of data to refresh its view of state each time?