Tv Eval

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.

specula-org 9aa550f 47 files · 660.2 KB Updated

File contents

Read guide.md for the full workflow.

Reference docs:

  • references/canonical_window_format.md — the one true window file schema
  • references/tv_module_template.md — how to write TV_.tla
  • references/score_interpretation.md — how to explain pass rates

Worked examples:

  • examples/spin/ — simple case (spinlock), 1 aux variable
  • examples/etcd/ — complex case (etcd-raft), 4 aux variables, log abstraction

specula-org/sysmobench/tree/main/tla_eval/skills/tv-eval commit 9aa550fd18

Frequently asked questions

npx skillmds@latest add specula-org/tv-eval