specula-org/Specula

code-analysis

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.

원문 언어: 영어

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.

원문 언어: 영어

writing-modeling-guidance

Writing target-specific modeling guidance for Specula. Use when: (1) the user is setting up Specula on a new target system, (2) the user asks to write or revise a guidance file, (3) the user wants to add scenario hypotheses, scope guidance, or…

원문 언어: 영어

bug-classification

Final reporting for Phase 4a results. Classify severity in bug-severity.md, then write a concise human-readable findings fragment for summary.md.

원문 언어: 영어

bug-confirmation

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…

원문 언어: 영어

harness-generation

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…

원문 언어: 영어

validation-workflow

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.

원문 언어: 영어

tla-checking-workflow

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…

원문 언어: 영어

tla-trace-workflow

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…

원문 언어: 영어