Testing the Proof System: Negative Controls and Dependency Evidence in Ota

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 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 --archiveota 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.

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.

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: validated and outcome: 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.

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 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.

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.

• Runtime Proof Evidence
• Contract Reference
• JSON Output Reference
• Execution Receipt
• Ota v1.6.24