Sharing a small TLA+ agent-skills repo

[Younes]

Hi all,

I wanted to share a small repo I’ve been working on:

https://github.com/younes-io/agent-skills

It provides two narrowly scoped TLA+ “Agent Skills”:

- tla-check: helps an agent create or refine .tla and .cfg files, run TLC, and report results with explicit bounds and assumptions
- tla-proof : helps an agent create or refine TLAPS proofs, run tlapm, and report what was proved, failed, or omitted

I’ve tried to make the workflows strict about honesty: "no counterexample found" is not "proved correct", and partial proofs are reported as partial proofs.

The repo works with Claude Code, and also with Codex and other coding agents that support the Agent Skills format.

My hope is that it may be useful for practical tasks like drafting a first spec, refining an existing one, or iterating on TLC/TLAPS failures. If anyone here looks at it, I’d be grateful for criticism, especially if it encourages the wrong habits or misrepresents good TLA+/TLAPS practice.

NB: Thanks as well to Markus, Stephan, and Karolis for a few comments that helped shape this.  

Best,
Younes