메뉴
Code analysis for formal verification. Use when: (1) investigating a system implementation to identify what to model in TLA+, (2) performing bug archaeology on a codebase, (3) producing a modeling brief that guides spec generation.
Codex 또는 Claude로 설치 이 Prompt를 복사해 Codex, Claude 또는 다른 어시스턴트에 붙여 넣으면 Skill 페이지를 검토하고 설치를 진행할 수 있습니다.
SOC 직업 분류 기준
Bug confirmation and reproduction. Use when: (1) a bug has been found by model checking and needs code-level validation, (2) reproducing a bug in the real system to confirm it is not a false positive, (3) assessing whether a TLA+ counterexample maps to a real triggerable scenario.
TLA+ Model Checking workflow. Use when: (1) running TLC model checking or simulation on a TLA+ spec, (2) analyzing counterexamples from invariant violations, (3) determining whether a violation is an invariant mismatch, a spec issue, or a real bug in the system implementation.
Severity classification of Phase 4a results. Assign severity to REPRODUCED bugs and ENV_LIMITED/MASKED findings, while recording non-severity dispositions such as FALSE POSITIVE, PENDING REPAIR, DEFERRED, and INCOMPLETE.
TLA+ Verification workflow (orchestration). Use when: running the full verification loop — iterating between trace validation and model checking until both pass, ensuring spec faithfully models the system.
Trace harness generation (Phase 2.5). Use when: (1) instrumenting a system's source code to emit NDJSON traces for TLA+ trace validation, (2) writing test scenarios that exercise protocol code paths, (3) producing the first batch of traces from instrumented tests.
TLA+ Trace Validation workflow. Use when: (1) validating if a trace matches a TLA+ spec, (2) debugging trace validation failures (TLC reports 'Temporal properties were violated' or validation stops unexpectedly), (3) fixing spec/trace inconsistencies after root cause is identified.
| name | code-analysis |
| description | Code analysis for formal verification. Use when: (1) investigating a system implementation to identify what to model in TLA+, (2) performing bug archaeology on a codebase, (3) producing a modeling brief that guides spec generation. |
Read guide.md for the full workflow methodology.
