메뉴
Resolve TLAPS proof failures involving theorem instances from modules with assumptions. Use when a citation such as BY I!Thm does not close a goal because prefixed and unprefixed imported operators are treated as different symbols.
기본적으로 소스를 먼저 확인하는 Prompt가 선택됩니다. 직접 명령으로 전환하거나 로컬 사본을 다운로드할 수도 있습니다.
설치 여부를 결정하기 전에 SKILL.md와 SkillsMP에 표시된 보조 파일을 읽어 보세요.
Codex 또는 Claude로 설치 이 Prompt를 복사해 Codex, Claude 또는 다른 어시스턴트에 붙여 넣으면 Skill 페이지를 검토하고 설치를 진행할 수 있습니다.
직접 명령은 검토 Prompt를 거치지 않습니다. 실행하기 전에 소스를 확인하세요.
npx skills add https://github.com/specula-org/tlaps-bench --skill tlaps-proof-hints명령은 한 줄로 유지됩니다. 복사하기 전에 가로로 스크롤해 전체 내용을 확인하세요.
로컬 사본을 원하시나요? SkillsMP에서 현재 제공할 수 있는 파일을 다운로드하세요.
Audit TLAPS Bench proof-completion tasks and cohorts for task integrity, theorem provability evidence, answer leakage, source-reference quality, difficulty signals, stale run artifacts, and model failure causes. Use when reviewing TLAPS task quality, trimming benchmark cohorts, investigating suspicious tasks, analyzing one-shot or agentic results, or preparing a shareable task-audit report.
Validate candidate inductive invariants for TLA+ safety proofs with Apalache or TLC. Use when designing or debugging an invariant, especially when TLAPS cannot discharge initiation, consecution, or safety-implication obligations.
SOC 직업 분류 기준
SKILL.md 표시 중
| name | tlaps-proof-hints |
| description | Resolve TLAPS proof failures involving theorem instances from modules with assumptions. Use when a citation such as BY I!Thm does not close a goal because prefixed and unprefixed imported operators are treated as different symbols. |
A citation such as BY I!Thm, NA does not close the goal even though I!Thm appears to prove it and NA appears to supply the corresponding local assumption.
When a module with assumptions is instantiated as I == INSTANCE M, the instantiated assumptions become hypotheses of its theorem instances. If an assumption mentions an operator imported through EXTENDS, the instance re-exports that operator under the I! prefix. TLAPS treats the prefixed and unprefixed names as distinct internal symbols, so backends do not automatically relate I!Pos(N) to Pos(N).
Prove a bridge theorem equating the prefixed operator with its local counterpart and cite it alongside the instantiated theorem:
---- MODULE Lib ----
EXTENDS Integers
Pos(n) == n > 0
====
---- MODULE A ----
EXTENDS Lib
CONSTANT N
ASSUME NA == Pos(N)
THEOREM Thm == N > 0
BY NA DEF Pos
====
---- MODULE B ----
EXTENDS Lib
CONSTANT N
ASSUME NA == Pos(N)
I == INSTANCE A
THEOREM Bridge == \A n : I!Pos(n) = Pos(n)
BY DEF I!Pos, Pos
THEOREM Test == N > 0
\* BY I!Thm, NA \* FAILS
BY I!Thm, NA, Bridge \* WORKS
====
Source: tlaplus/tlapm#279