younes-io
@younes-io
Public Skills
tlaps-workbench
by younes-io
"Write and iteratively refine TLA+ theorem proofs in .tla modules with TLAPS (tlapm); run proof checks and summarize proved vs failed/omitted obligations with explicit assumptions and trust boundaries. Use when asked to create/fix THEOREM or PROOF blocks, diagnose TLAPS failures, tune proof decomposition/tactics/backends, or report theorem-proving progress."
tlaplus-workbench
by younes-io
"Write and iteratively refine executable TLA+ specs (.tla) and TLC model configs (.cfg) from natural-language system designs; run TLC model checking; summarize pass/fail and counterexamples with explicit assumptions and bounds. Use when asked to: design/validate a state machine or distributed protocol with TLA+, create/edit .tla or .cfg files, run TLC, or interpret TLC failures/counterexamples."