Implement and verify design doc invariants by annotating tests and source code with [INV-*] / @spec tags, then driving tx spec coverage from BUILD toward HARDEN (100% FCI). Works with any design doc that has an invariants block.
Instalar con Codex o Claude Copia este prompt, pรฉgalo en Codex, Claude u otro asistente, y deja que revise la pรกgina de la skill y la instale por ti.
Un comando directo omite el prompt de revisiรณn. Revisa el origen antes de ejecutarlo.
Implement and verify design doc invariants by annotating tests and source code with [INV-*] / @spec tags, then driving tx spec coverage from BUILD toward HARDEN (100% FCI). Works with any design doc that has an invariants block.
Verify Invariants
Drive invariants from uncovered (BUILD phase) to fully verified (HARDEN phase) by annotating integration tests and source code with invariant IDs.
Scope:
With argument (e.g. /verify-invariants team-tags-design): verify that doc only
Without argument (/verify-invariants): verify ALL design docs and PRDs with uncovered invariants
How tx spec Discovery Works
tx spec discover scans files in two passes:
Test files (matched by test_patterns in .tx/config.toml) โ scanned for both [INV-*] bracket tags in test names AND // @spec INV-* comments
Source files (all programming languages) โ scanned ONLY for // @spec INV-* comments (structural annotations)
This means @spec comments work in ANY file (test or source), but [INV-*] bracket tags are only picked up from test files.
Annotation Formats
Format
Where It Works
Example
[INV-TAG-001] in test name
Test files only
it('creates tag [INV-TAG-001]', ...)
// @spec INV-TAG-001 comment
Any file (test or source)
above a schema definition
// @spec INV-TAG-001
-- @spec INV-TAG-001 SQL comment
.sql files
-- @spec INV-TAG-001 in pgTAP test
# @spec INV-TAG-001 hash comment
.py, .rb, etc.
# @spec INV-TAG-001 above a test
Critical: IDs Are Case-Sensitive
INV-TAG-001 and inv-tag-001 are NOT the same. Always use UPPERCASE as shown in the design doc's invariants: YAML block.
Critical: Config Matters
The test_patterns in .tx/config.toml control which files are scanned as test files. The defaults include:
test_patterns = [
"**/*.test.{ts,js,tsx,jsx}",
"**/*.integration.test.{ts,js,tsx,jsx}",
"**/*.spec.{ts,js,tsx,jsx}",
"**/*.pgtap.sql",
# ... and more for Go, Python, Rust, Java, Ruby, C/C++
]
If your test file isn't being found, check that its pattern matches one of these globs.
Workflow State Machine
START
โ
โผ
โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ
โ Step 1: LOAD GAPS โ
โ โ
โ If <name> given: โ
โ tx spec gaps --doc <name> โ
โ tx spec fci --doc <name> โ
โ tx doc show <name> --md โ
โ โ
โ If NO argument: โ
โ tx spec gaps (all docs) โ
โ tx spec fci (global) โ
โ tx doc list (enumerate all docs) โ
โ For each doc with gaps: โ
โ tx doc show <doc> --md โ
โ โ
โ โโ FCI = 100%? โ Already HARDEN. Done. โ
โ โโ FCI < 100%? โ Continue to Step 2 โ
โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ
โ
โผ
โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ
โ Step 2: CLASSIFY INVARIANTS โ
โ โ
โ For each uncovered invariant, decide: โ
โ โ
โ A) TESTABLE โ can be verified by an integration โ
โ test or unit test exercising the behavior. โ
โ Examples: API returns 401, cascade deletes, โ
โ filter returns correct results. โ
โ โ Annotate in test file with [INV-*] tag โ
โ โ
โ B) STRUCTURAL โ enforced by code structure, lint, โ
โ or DB constraint. Cannot be meaningfully tested โ
โ in isolation but IS enforced in source. โ
โ Examples: "tag names unique per org" enforced โ
โ by DB index, "no retention policy" enforced by โ
โ absence from retentionTableNames literal. โ
โ โ Annotate in source code with // @spec INV-* โ
โ โ
โ C) PGTAP โ enforced by database constraints. โ
โ โ Annotate in pgTAP test with -- @spec INV-* โ
โ โ
โ Prefer A over B. Use B only when A is genuinely โ
โ not possible. โ
โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ
โ
โผ
โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ
โ Step 3: IMPLEMENT + ANNOTATE โ
โ โ
โ For TESTABLE invariants: โ
โ Write or extend integration test files. โ
โ Annotate each test with the invariant ID: โ
โ โ
โ it('creates tag [INV-TAG-001]', async () => { โ
โ // test body โ
โ }) โ
โ โ
โ OR use comment form: โ
โ // @spec INV-TAG-001 โ
โ it('creates tag', async () => { ... }) โ
โ โ
โ For STRUCTURAL invariants: โ
โ Place // @spec comment in the source file where โ
โ the invariant is enforced (schema, literals, etc.) โ
โ โ
โ For PGTAP invariants: โ
โ Place -- @spec comment in the .pgtap.sql file โ
โ โ
โ RULE: Every invariant must get exactly one โ
โ annotation somewhere in the codebase. โ
โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ
โ
โผ
โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ
โ Step 4: DISCOVER โ
โ โ
โ tx spec discover --doc <name> โ
โ tx spec discover (if verifying all) โ
โ โ
โ Verify output shows: โ
โ Scanned N file(s) โ
โ Discovered links: M โ
โ By source: tag=X, comment=Y โ
โ โ
โ If 0 links: check annotation format, file path, โ
โ config.toml patterns, ID case sensitivity. โ
โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ
โ
โผ
โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ
โ Step 5: RUN TESTS + RECORD RESULTS โ
โ โ
โ For vitest tests: โ
โ pnpm vitest run <file> --reporter=json โ
โ 2>/dev/null | tx spec batch --from vitest โ
โ โ
โ For structural annotations: โ
โ tx spec run "<file>::spec@line-N" --passed โ
โ โ
โ For pgTAP: โ
โ pnpm test:db:pgtap โ
โ tx spec run "<pgtap-file>::<test>" --passed โ
โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ
โ
โผ
โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ
โ Step 6: CHECK PROGRESS โ
โ โ
โ tx spec fci --doc <name> โ
โ tx spec gaps --doc <name> โ
โ โ
โ โโ FCI = 100% โ HARDEN phase reached. Done. โ
โ โโ Gaps remain โ Loop back to Step 3 for remaining. โ
โ โโ Failures โ Fix failing tests, re-run Step 5. โ
โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ
โ
โผ
โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ
โ Step 7: REPORT โ
โ โ
โ tx spec matrix --doc <name> โ
โ tx spec status --doc <name> โ
โ โ
โ Print summary with invariant coverage breakdown. โ
โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ
โ
โผ
DONE
verified_by โ hint about which test file should cover it
traces_to โ which PRD requirement it maps to
If FCI is already 100%, report success and stop.
Step 2 โ Classify Each Uncovered Invariant
For each gap from tx spec gaps, decide the verification strategy:
Category
When to use
Annotation style
Where
TESTABLE
Behavior can be exercised via API call, function call, or DB query
[INV-*] in test name or // @spec INV-* near test
Test file (.test.ts, .integration.test.ts, .pgtap.sql)
STRUCTURAL
Enforced by schema, lint rule, type system, or code structure โ no meaningful test possible
// @spec INV-* comment
Source file where enforcement lives (schema.ts, literals.ts, service file)
PGTAP
Database constraint, trigger, or index behavior
-- @spec INV-* SQL comment
.pgtap.sql test file
Prefer TESTABLE. Most invariants should be verifiable by a test. Only use STRUCTURAL when the invariant is genuinely about code structure (e.g., "table X is NOT in retentionTableNames" โ verified by inspecting the literal array, not by running a test).
Step 3 โ Implement and Annotate
Integration test annotation (preferred)
The [INV-*] bracket tag in the test name is the cleanest approach โ tx spec discover extracts both the invariant ID and the test name from the same line:
it('creates tag with name and color [INV-TAG-001]', async () => {
const res = awaitfetch(`${ctx.baseUrl}/v1/organizations/${orgId}/tags`, {
method: 'POST',
headers: { 'content-type': 'application/json', authorization: `Bearer ${adminToken}` },
body: JSON.stringify({ name: 'Engineering', color: '#3B82F6' })
})
expect(res.status).toBe(201)
})
The comment form also works โ place it on the line immediately before or up to 2 lines above the it():
// @spec INV-TAG-100it('returns 401 without auth token', async () => {
const res = awaitfetch(`${ctx.baseUrl}/v1/organizations/${orgId}/tags`)
expect(res.status).toBe(401)
})
Source code annotation (structural)
tx spec discover scans ALL source files (any language) for @spec comments. Place the annotation directly above the code that enforces the invariant:
Important: Structural annotations create a link with a test ID like packages/infra/db/src/schema.ts::spec@line-264. You must manually record these as passed since there's no test to run:
# Get the exact test ID
tx spec tests INV-TAG-200
# Output: packages/infra/db/src/schema.ts::spec@line-264 [comment]# Record as passed
tx spec run "packages/infra/db/src/schema.ts::spec@line-264" --passed
pgTAP annotation
-- @spec INV-TAG-202SELECT ok(
EXISTS (
SELECT1FROM pg_constraint
WHERE conname ='team_tag_assignments_tag_id_fkey'AND confdeltype ='c'
),
'tag assignments cascade-delete when tag is deleted'
);
Rules
Every invariant gets exactly one annotation somewhere in the codebase
One test/annotation can cover multiple invariants: [INV-TAG-001] [INV-TAG-002]
Critical severity invariants should be covered first
Integration tests are preferred over unit tests (hard requirement from design doc skill)
Step 4 โ Discover
# For a specific doc
tx spec discover --doc $ARGUMENTS# For all docs
tx spec discover
Test patterns in .tx/config.toml don't match your test files
Add patterns like "**/*.test.{ts,js}" or "**/*.integration.test.{ts,js}"
Scanned files but 0 links
Annotation format wrong
Must be [INV-TAG-001] (with brackets) or // @spec INV-TAG-001 โ no other formats work
Links found but wrong count
ID mismatch
IDs are case-sensitive. INV-TAG-001 is not inv-tag-001 or INV-Tag-001
Source @spec not found
Source file excluded
Check file isn't in node_modules, dist, .git, or other skip dirs
How Test IDs Are Built
tx spec discover builds test IDs as {relative-file-path}::{test-name}. For example:
apps/api/src/routes/team-tags.test.ts::creates tag with name and color [INV-TAG-001]
packages/infra/db/src/schema.ts::spec@line-264 (structural โ no test name, uses line number)
Step 5 โ Run Tests and Record Results
Vitest (primary path)
# Run specific test file and pipe JSON results to tx
pnpm vitest run apps/api/src/routes/team-tags.test.ts --reporter=json 2>/dev/null | tx spec batch --from vitest
tx spec batch --from vitest does the following:
Parses the vitest JSON report
Normalizes absolute file paths to relative (strips repo root)
Matches test results to discovered spec_tests by {file}::{title}
Records PASS/FAIL runs for each matched invariant
Important: vitest outputs absolute paths but tx spec discover stores relative paths. The batch parser handles this automatically by stripping common path prefixes (/apps/, /packages/, /src/, etc.).
Important: vitest fullName includes describe ancestry (e.g. suite name > test name) but discover stores just the it() title. The batch parser emits both variants and matches on the title (shorter form) first.
Structural annotations (manual recording)
Structural annotations (source code @spec comments) have no test to run. After confirming the code correctly enforces the invariant, record them manually:
# Get the exact test ID from tx spec tests
tx spec tests INV-TAG-200
# Output: packages/infra/db/src/schema.ts::spec@line-264 [comment]# Record as passed
tx spec run "packages/infra/db/src/schema.ts::spec@line-264" --passed
pgTAP tests
# Run pgTAP suite
pnpm test:db:pgtap
# Record results manually (pgTAP doesn't output vitest-compatible JSON)
tx spec run "packages/infra/db/pgtap/003_team_tags.pgtap.sql::cascade delete" --passed
All invariants linked + passing โ ready for sign-off
100% + sign-off
COMPLETE
Human confirmed feature is done
What "untested" Means
tx spec fci distinguishes between:
covered โ invariant has a linked test/annotation (via discover)
passing โ linked test has a recorded PASS run (via batch or manual)
untested โ covered but no run recorded yet
A common state is covered=14, passing=12, untested=2 โ meaning 2 invariants are linked (discovered) but you haven't yet run tx spec run --passed for them. This typically happens with structural annotations.
Iteration Loop
If gaps remain:
Check which invariants are uncovered: tx spec gaps --doc <name>
Add the missing annotation (test or source)
Re-run tx spec discover
Run tests + record results
Check FCI again
Step 7 โ Report
tx spec matrix --doc $ARGUMENTS
tx spec status --doc $ARGUMENTS
The matrix shows every invariant with its linked test and latest result:
INV-TAG-001: Organizations can create, list, update, and delete tags via API
- apps/api/src/routes/team-tags.test.ts::creates tag [INV-TAG-001] [tag] latest=PASS
INV-TAG-200: Tag names are unique per org via DB index
- packages/infra/db/src/schema.ts::spec@line-264 [comment] latest=PASS
Print a summary:
Total invariants
Covered by test annotations vs source annotations
FCI percentage and phase
Any remaining gaps or failures
After Verification
FCI = 100% โ phase is HARDEN. All invariants are mechanically verified.
Human sign-off: tx spec complete --doc <name> --by <name> โ moves to COMPLETE.
Regression detection: Re-run tests periodically โ tx spec batch โ FCI drops if a test fails, phase reverts to BUILD.
Proven Example (team-tags-design)
This workflow was tested end-to-end with the team-tags-design doc:
14 invariants (design doc)
โ tx spec discover
12 [INV-*] tags in test file + 2 @spec comments in schema.ts = 14 links
โ vitest run | tx spec batch --from vitest
12 test results recorded (PASS)
โ tx spec run --passed (2 structural)
2 structural results recorded
โ tx spec fci
FCI: 100% (HARDEN)
โ tx spec matrix
All 14 invariants โ PASS
