Read guide.md for the full workflow.
Reference docs:
references/canonical_window_format.md— the one true window file schemareferences/tv_module_template.md— how to write TV_.tlareferences/score_interpretation.md— how to explain pass rates
Worked examples:
examples/spin/— simple case (spinlock), 1 aux variableexamples/etcd/— complex case (etcd-raft), 4 aux variables, log abstraction