Per docs/src/architecture/status.md, the soundness tests check internal consistency only (storage-backend agreement, determinism, parser roundtrip) — there is no external oracle. Past spurious/hidden-violation bugs in symmetry/POR (closed #56, #60, #82) show this class recurs. Add a CI differential that runs the example corpus through both specl and TLC (the translator already exists) and diffs OK/violation verdicts and, where feasible, state counts. This is the highest-value assurance investment for the checker.
Per docs/src/architecture/status.md, the soundness tests check internal consistency only (storage-backend agreement, determinism, parser roundtrip) — there is no external oracle. Past spurious/hidden-violation bugs in symmetry/POR (closed #56, #60, #82) show this class recurs. Add a CI differential that runs the example corpus through both specl and TLC (the translator already exists) and diffs OK/violation verdicts and, where feasible, state counts. This is the highest-value assurance investment for the checker.