A green call does not prove the dependency mattered
A service can be reachable without being exercised. An application can call a dependency without
proving the dependency shaped the tested obligation. A control can fail for an unrelated reason.
Flatten those outcomes into one green or red status and a proof system will eventually claim more
than it observed.
Ota 1.6.24 separates three levels:
-
reachable: the selected path reached a declared dependency boundary; -
exercised: a finite observer recovered evidence produced through that dependency in the current proof transaction; -
fault_tested: a separate control proved the same obligation failed for the declared missing-effect reason.
Each level answers a different question. None may be inferred from a command label or exit code.
The contract names the seam and the control
The runtime workflow declares the positive observation and the negative control independently:
workflows:
app-proof:
run:
task: app
readiness:
surfaces: [app]
proof:
seam_observations:
- id: postgres-marker
dependency: postgres
producer_task: proof:marker-produce
task: proof:marker-observe
marker_env: OTA_PROOF_DEPENDENCY_MARKER
negative_controls:
- id: postgres-unavailable
dependency: postgres
obligation: postgres-marker
task: proof:postgres-unavailable
intervention:
kind: dependency_endpoint_override
expected_failure: dependency_unavailable
Run the ordinary proof first. Select the control explicitly when the causal claim is required:
ota proof runtime --workflow app-proof --json --archive
ota proof runtime --workflow app-proof \
--negative-control postgres-unavailable \
--json --archive
Ota does not silently inject failure into every runtime check. Negative controls are separate proof
runs because they answer a stronger question and may mutate or disrupt the selected dependency.
exercised requires current-transaction evidence
The do-nothing observer is the first adversary.
If an observer can exit zero without reading evidence from the dependency, it has not proved the
seam was exercised. If it can reuse a value from yesterday's run, it has not proved this execution
used the seam.
For marker-bound observations, Ota creates an opaque marker and gives it only to the declared
producer. The observer receives the transaction context but not the marker. It must recover the
marker through the dependency and write the runner-owned attestation.
Ota verifies the observation identity, transaction identity, marker, and evidence digest before it
emits level: exercised. The transient marker is then removed. A clean observer exit, guessed
value, stale record, or caller-side trace cannot earn that level.
fault_tested requires the right red
The negative control has its own adversary: an unrelated failure.
A broken setup step, timeout, DNS failure, crash, or generic non-zero exit may turn the lane red. It
does not prove that removing PostgreSQL invalidated the same obligation that passed in the green
run.
Ota promotes the seam only when the canonical control record is:
- bound to the same proof transaction and obligation;
- run under the declared intervention;
- classified as
expected_missing_effect; - backed by a matching failure-attestation digest;
- emitted with
status: validatedandoutcome: expected_obligation_failed.
The dependency record carries only a derived projection of that canonical control. This prevents a
nested object from becoming a second, weaker authority.
{
"dependency_evidence": [
{
"dependency_id": "service:postgres",
"proof_obligation_id": "postgres-marker",
"level": "fault_tested",
"observation": {
"origin": "round_trip_effect",
"evidence_class": "attested"
},
"negative_control": {
"status": "validated",
"same_obligation": true,
"failure_mode": "expected_missing_effect",
"failure_attestation_digest": "sha256:..."
}
}
]
}
If Ota cannot validate that chain, the control remains invalid or unrun. An unclassified red
never upgrades evidence to fault_tested.
Strong seam proof is still bounded proof
A PostgreSQL marker round trip can establish that the selected obligation depended on PostgreSQL.
It cannot establish that PostgreSQL shaped every response, migration, query result, or user-visible
output in the repository.
Ota therefore retains the obligation-scoped boundary:
{
"proof_verdict": "passed_with_unproven_boundaries",
"not_proved": [
{
"kind": "dependency_output_shaping_not_proved",
"proof_obligation_id": "postgres-marker"
}
]
}
This is not a caveat hidden in prose. It travels with the artifact so CI and agents cannot honestly
turn one controlled seam into repo-global proof.
Athena API supplied the real pressure
athena-api forced this model through a Rails and
PostgreSQL runtime rather than a synthetic fixture. Its released Ota 1.6.24 matrix
run #29572074325 proved native and
container lanes while keeping Windows intentionally static. The later PostgreSQL pressure retained
dependency_output_shaping_not_proved even after the marker-bound seam and matching control became
stronger.
Read the full engineering note: Pressure-testing Ota on athena-api.
The design rule
Proof must be able to fail its own strongest claim.
Reachability proves contact. Transaction-bound observation proves the selected seam was exercised.
A validated same-obligation control proves the dependency was necessary for that obligation. Ota
keeps those claims separate because automation becomes dangerous when evidence levels collapse into
one optimistic green.
References
Originally published here: https://ota.run/blog/testing-the-proof-system-negative-controls-and-dependency-evidence
