verification: formal methods skill (TLA+, Lean) #7561

Parent

Refs #7555. Source: PLAN Phase 0, topic poteto-review. Thread: Formal methods (TLA+, Lean)
(deferred).

Depends on

• none (parked: opens on the reopen trigger below, not on an edge)

Reopen trigger

The recorded revisit trigger in this repo's tlaplus-agentskills upstream record: a loop-lane
concurrency bug a model would have caught, or a consumer asks.

Outcome

When reopened: a decision on a TLA+ or Lean skill.

Decisions

• No change now; deferred with its revisit trigger; /verification:confirm points to the
  formal-methods spectrum (D15; the pointer ships in the verification and implementation thread).
  Origin: ours.
• Options on record: a TLA+ skill now, declined until a trigger fires.

Key interfaces

None (deferred, no module change yet).

Done when

• The trigger has fired and is cited in a comment.
• A decision is recorded and any slices are filed under this item.

Out of scope

• The spectrum pointer in /verification:confirm, which the verification and implementation
  thread ships.