[tlaplus] Re: Cursor's pstack plugin defaults to TLA+ for model checking

[Younes <younesagma@xxxxxxxxx>]

TLA+ is also mentioned here : https://github.com/cursor/plugins/blob/d457567332aa6989e753ea289f30ea2bfbc80bc0/pstack/docs/guide/06-verify-and-ship.md#prove-a-property-with-a-formal-verification-skill

On Monday, October 19, 2026 at 5:54:32 AM UTC Younes wrote:

Hi all,

pstack, a plugin in Cursor's official plugins repo, has a formal-verification skill (still in beta) for coding agents. For checking whether events can happen in a bad order, it names TLA+ as the default in any language:

https://github.com/cursor/plugins/blob/d457567332aa6989e753ea289f30ea2bfbc80bc0/pstack/skills/create-formal-verification-skill/SKILL.md

Thought the group would like to know.

Best,
Younes

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/b4f3dcd7-453a-4498-832e-965673aa9ce6n%40googlegroups.com.