Check reference

Connect tests to the promises they examine

A test can run successfully without making clear which promise it checks. An orphan-test review connects its setup and assertions to the appropriate requirement, or exposes a gap in the specification.

What the check observes

In source-native mode, recognized test functions need requirement ownership through eligible annotations or authored verification targets. An annotation on one function does not automatically own its neighbors. Go Test and Fuzz functions are evidence candidates; Benchmark and Example functions are not orphan tests by default, though they can explicitly opt into requirement evidence. In overlay-audit mode, this source-annotation gate returns a policy pass without scanning orphan tests. Separate overlay evidence checks must establish the accepted external bindings; the pass here does not validate them.

An unlinked test is still useful work

CaseWhat to inspectAppropriate response
A real test has assertions but no ownership link.Which product promise do the setup and assertions exercise?Keep the test and establish the correct link, or identify missing intent.
A neighboring test is annotated.Does this function have its own recognized scope or an eligible explicit file-level declaration?Do not infer ownership merely from proximity.
Go Benchmark or Example without an evidence declaration.Is this a performance experiment or documentation example rather than declared requirement evidence?These are not orphan-test candidates by default; explicit evidence declarations can opt them in.
A named test passes but the requirement is wrong.Where did the expected result come from?Review the requirement and assertion; an ownership check cannot resolve this.

The scan classifies recognized test functions; it does not run them. Go setup such as TestMain and an ordinary helper merely named TestSomething outside a test file are not automatically product tests. Inspect the reported symbol and language rules before adding a trace annotation.

Example: a new test inherits no ownership

Illustrative case. An existing annotated test checks the valid request path. A second test is added for expired credentials. Its proximity in the file does not link it to the same requirement, and the rejection behavior may need its own obligation.

// Verifies: SYS-REQ-042
func TestValidRequest(t *testing.T) { /* call and assert */ }

// Review the correct requirement before annotating this test.
func TestExpiredCredentials(t *testing.T) { /* call and assert */ }

Resolve the finding

  1. Read what each reported test actually asserts, including the failure it is meant to detect.
  2. Link it to the governing requirement and relevant obligation at the correct function or file scope. Confirm the target remains current after supersession.
  3. For test infrastructure with no product evidence role, use a justified scope decision. Do not delete useful tests or invent requirement links to clear the count.

Run and interpret

proof lint --check orphan_tests_clean

Orphan checks default to scanning all recognized source files. Traced-only scans disclose skipped files and can warn that breadth is unassessed. Source-native and overlay-audit policies deliberately have different ownership expectations.

Ownership does not mean the test executed, passed, or has an adequate oracle. Stale target resolution and annotation validity also need their own checks. A passing orphan scan cannot establish that every requirement has a test, because it starts from the tests that exist.

Continue from here

Start tests from expected behavior. Check test grounding.

Bring a test suite whose requirement coverage is hard to explain. Bring a change to Proof.