Contract proof demo

Contract. Counterexample. Proof of fix.

A vulnerable admin route is accepted only after a deterministic counterexample proves the baseline violated the contract and the fixed runtime passes the same replay.

This proves this route and replay, not the whole repo.

FAIL missing-authz

Agent creates public admin route

Unauthenticated GET /admin/users returns 200 on the vulnerable runtime.

CONTRACT created

Observable safety contract

Unauthenticated request must receive 401 or 403.

REPLAY baseline got 200

Counterexample reproduced

The same JSON replay proves the unsafe baseline is actually reachable.

FIX applied

Auth middleware added

The agent can patch the route, but the model does not get to declare victory.

REPLAY fixed got 401

Same replay, fixed runtime

The oracle reruns the unauthenticated request and observes denial.

PASS scoped acceptance

Accepted only for this route

Baseline fail plus fixed pass creates evidence for this route and replay.