# 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.

- Skill: `specula-org/tv-eval` (Agent Skill, multi-file: 47 files)
- Install (CLI): `npx skillmds@latest add specula-org/tv-eval`
- Raw SKILL.md: https://api.skillmd.com/api/skills/specula-org/tv-eval/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: AI & ML
- Author: specula-org (https://skillmd.com/u/specula-org)
- Updated: 2026-09-17
- Page: https://skillmd.com/skills/specula-org/tv-eval

---


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_<Action>.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