Show HN: TLA+ Workbench skill for coding agents (compat. with Vercel skills CLI)

Show HN: TLA+ Workbench skill for coding agents (compat. with Vercel skills CLI)(github.com)

41 points by youio 85 days ago | 4 comments

youio 85 days ago |

I built a TLA+ skill for coding-agent workflows.

This repo currently focuses on one skill: tlaplus-workbench. It helps convert natural-language designs into .tla/.cfg files, run TLC, and summarize counterexamples.

Quick try: npx -y skills add younes-io/agent-skills --skill tlaplus-workbench

List skills from a local checkout: npx -y skills add . --list

TLA+ spec examples (generated from one-shot prompts): https://github.com/younes-io/tlaplus-workbench-examples

Feedback I'd value: 1. Is this useful for real protocol/state-machine modeling? 2. What features should I add next for this TLA+ skill?

erichocean 84 days ago | |

I would give it every example TLA+ file you can find, including PlusCal stuff (as reference). Also provide an up to date language manual and/or grammar if you have one.

whattheheckheck 84 days ago |

Do you think it helps with the systems reasoning? Are there many tla+ specs + real code bases for the llm to learn from?

section_me 84 days ago | |

Raft is a good example. And it seems to be in most models training data.