Comment by zozbot234

There is no contradiction here, TLA+ is mostly about proving properties of toy models, not end-to-end proofs about real programs. As TLA+ practitioners like to point out, the latter is only applicable to favorable "local" properties - this is what type systems do, they state claims that are quite aligned with the program's syntactic structure; or else to rather trivial programs where proving "whole-program" claims is still feasible. Even Verus itself doesn't really change this.