Profile My skills Saved Collections Edit profile Submit a skill

← all publishers

specula-org

@specula-org source repo

7 published skills

  1. ▌
    Tv Eval · specula-org bundle
    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.
    0
    installs
  2. ▌
    Harness Gen · specula-org bundle
    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.
    0
    installs
  3. ▌
    Tlaps Proof Hints · specula-org
    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.
    0
    installs
  4. ▌
    Tlaps Task Audit · specula-org bundle
    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.
    0
    installs
  5. ▌
    Tla Inductive Invariant Validation · specula-org
    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.
    0
    installs
  6. ▌
    Bug Classification · specula-org bundle
    Final reporting for Phase 4a results. Classify severity in bug-severity.md, then write a concise human-readable findings fragment for summary.md.
    0
    installs
  7. ▌
    Incremental Modeling · specula-org bundle
    Incrementally evolve and verify an existing Specula TLA+ suite for a new source revision. Use when an Agent has a prior Specula run plus old and new source, and must decide whether the model changes, update the reference/MC/Trace suite, generate Update.tla, reuse and rebase the prior trace harness for update-focused validation, model-check changed/unchanged interactions, and hand real counterexamples to bug reproduction.
    0
    installs