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

Activity

1. kyle-sexton

   added

   needs-humanHuman-in-the-loop required; autonomous sessions must not resolve items carrying this.Human-in-the-loop required; autonomous sessions must not resolve items carrying this.

   on Oct 16, 2026
2. kyle-sexton

   added a parent issue on Oct 16, 2026

   • Epic: absorb Lauren Tan's and Matt Pocock's agent workflows (poteto-review) #7555
3. kyle-sexton

   added the

   Feature

   issue type on Oct 16, 2026
4. kyle-sexton

   set

   Work status

   to

   needs-spec

   on Oct 16, 2026
5. github-actions commented on Oct 16, 2026

   

   github-actionsBot

   on Oct 16, 2026 – with GitHub Actions

   Last edited by github-actions

   Contributor

   More actions

   Proposed work class: none

   Size: Small
   Complexity: Low
   Uncertainty: Known
   Flags: intent

   I understand this as a parked item. It tracks a possible TLA+ or Lean formal-methods skill. It reopens only when its trigger fires: a loop-lane concurrency bug a model would have caught, or a consumer asking. The issue body does not cite a fired trigger, and the comment does not cite one either.

   Open questions:

   1. Has the reopen trigger fired? RECOMMENDED: No, keep it parked. Nothing on the issue cites a qualifying bug or consumer request.
   2. If it has fired, should the outcome be a TLA+ skill, a Lean skill, or neither? RECOMMENDED: Decide TLA+ first. The recorded option on file is TLA+, and concurrency bugs are the stated trigger.

   I know of no duplicates.

   _{Automated triage. A maintainer reviews it.}
6. github-actions

   changed the issue type from

   Feature

   to

   Task

   on Oct 16, 2026
7. kyle-sexton

   changed the issue type from

   Task

   to

   Feature

   on Oct 16, 2026
8. kyle-sexton

   added

   needs-specNeeds a Brief or plan before anyone can build it.Needs a Brief or plan before anyone can build it.

   on Oct 16, 2026
9. kyle-sexton

   removed

   needs-humanHuman-in-the-loop required; autonomous sessions must not resolve items carrying this.Human-in-the-loop required; autonomous sessions must not resolve items carrying this.

   on Oct 24, 2026
10. kyle-sexton commented on Oct 24, 2026

    

    kyle-sexton

    on Oct 24, 2026

    MemberAuthor

    More actions

    Released for re-triage under the owner's 2026-10-24 rule: an issue stops for a person only for an intent or vision question, a security call, a host or attended run, or spend outside prepaid credit. The hold label came off and intake triage runs again now; it re-applies a hold, with a numbered question, when one of those applies.

    To hold this issue again, add needs-human (or status: needs-decision) and say why in a comment.
11. github-actions

    added

    priority: lowNice-to-have, cosmetic, or speculative; opportunistic.Nice-to-have, cosmetic, or speculative; opportunistic.

    status: needs-decisionAwaiting a human or maintainer judgment call.Awaiting a human or maintainer judgment call.

    needs-triageNot yet classified. Floor until a type and one priority tier are set.Not yet classified. Floor until a type and one priority tier are set.

    on Oct 24, 2026
12. melodic-automation-lanes commented on Oct 24, 2026

    

    melodic-automation-lanesBot

    on Oct 24, 2026

    Contributor

    More actions

    Refinement. A read-only run explored this repository, searched its issues and pull requests, and read the allowed docs to draft what follows. It is model text, to check, not instructions.

    Intended outcome: Stay parked: no TLA+ or Lean skill is added until the revisit trigger fires and a comment cites it.

    Related work

    • verification: intent chain, pstack ready rules and dispatch brief #7587 (related): verification thread issue on the intent chain; the confirm formal-methods spectrum pointer ships in that thread, not here
    • Concise skills rollout: verification (3 skills, 2 model-invoked) #6593 (related): verification skills rollout that the deferred formal-methods skill would extend

    Open questions

    1. Has the reopen trigger fired (a loop-lane concurrency bug a model would have caught, or a consumer asking)?
       RECOMMENDED: No. Keep it parked: nothing on the issue cites a qualifying bug or consumer request, and the first done-when item needs one. Basis: docs/upstream/tlaplus-agentskills.md:34
    2. If the trigger fires, should the outcome be a TLA+ skill, a Lean skill, or neither?
       RECOMMENDED: Decide TLA+ first, since the option on record is TLA+ and concurrency bugs are the stated trigger. Basis: judgment
    3. Should this issue be closed or labeled as parked, since the done-when items need a fired trigger that an unattended run cannot produce?
       RECOMMENDED: Keep it open with a parked label and no lane work until a person cites the trigger. Basis: judgment

    Sources read

    • /home/runner/work/_temp/refine-data/context.json: issue 7561 is parked, cites no fired trigger, and triage found no duplicates
    • docs/upstream/tlaplus-agentskills.md:29: a later skill would be ours if the revisit trigger fires and a skill is warranted
    • docs/upstream/tlaplus-agentskills.md:34: holds the Revisit trigger section that reopens the decision
    • docs/upstream/cursor-pstack.md:349: records that no plugin here ships a model-invoked TLA+ skill

    _{Automated refinement by the lanes App. Answer with a comment whose first line is **Decision recorded.**.}