A TLA+ primer states what model checking leaves uncovered, and reports 3,000 machine-checked Verus proofs from 16,459 specification pairs

Sources: primary, discussion
Summary: The post is explicit about the three places TLA+ stops short, which is the part most introductions omit. TLC enumerates a finite instance only, and the leader-election example grows from 38 states at three nodes to over a million at nine, the specification is a separate model that can drift from the implementation, and linear temporal logic cannot state branching or strategic properties. The pipeline result of 3,000 machine-checked Verus proofs from 16,459 specification pairs is the company's own claim, with follow-up posts promised and no dataset or evaluation set released yet, and the post is also a hiring and product pitch.
Why it matters: The primer and its stated limits are the durable part, because a team deciding whether to specify needs the coverage boundary before the tutorial.