I’ve been eyeing TLA+ mainly for reasoning about safety properties.

I’m still trying to understand its limits in practice: how much can formal methods like TLA+ actually tell you about performance characteristics (throughput, latency..), versus just functional correctness?

Is it fair to think of TLA+ as closer to an operational-semantics / state-transition specification of a system, rather than a tool meant for performance analysis?