specula-org

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.

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+ 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 a spec issue, an overly-strong invariant, or a real bug in the system implementation.

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.

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.

Severity classification of bugs already confirmed by Phase 4a. Use when: (1) Phase 4a (bug-confirmation) has produced confirmed-bugs.md and each entry needs a Severity tier, (2) producing the input for downstream submission filtering, (3) re-classifying bugs after status changes (e.g., REPRODUCTION FAILED → REPRODUCED on retry).

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.

TLA+ spec generation from a modeling brief. Use when: (1) turning code analysis findings into a TLA+ specification, (2) generating model checking and trace validation specs, (3) producing instrumentation mappings for trace collection.

Transition validation (TV) for TLA+ specs. Use when: scoring how faithfully an AI-generated spec models a real system, producing per-action pass rates with defensible explanations. The agent acts as the examiner (考官) — writes instrumentation, runs harness, writes TV modules, runs TLC, and interprets scores.

Trace harness generation for SysMoBench. Use when bootstrapping a new task: clone the system into artifacts/<task>/, instrument it to emit NDJSON traces at the task-required granularity, write a run.sh, and produce INSTRUMENTATION.md. One-time work per task; the resulting harness is reused for every spec evaluation via the tv-eval skill.

Bounded repair of TLA+ specs that fail P1 (SANY) or P2 (TLC from Init). Use when a model-generated spec needs to pass P1/P2 so downstream P3 (TV) and P4 (invariant) can score it. Enforces a strict allow-list of mechanical fixes and MUST NOT alter the model's semantic intent (actions, guards, variable set). Every edit must carry a written justification.