sots-re/campaign/rollout/formal-verifier-state.md

# Controls formal verifier checkpoint

## Fresh verifier quantum plan — run-cb15199f9272fe496bd10a8a

Actor `controls-independent-verifier`; role `verifier`; requested model
`openai/gpt-5.6-terra`; session `run-cb15199f9272fe496bd10a8a`. This is an
independent re-execution, scoped only to `controls-bootstrap` /
`controls-negative-paths`; it is neither original-assisted validation nor a
partial/full engine comparison, independent replacement, or integrated replay.

Falsifiers defined before execution: (1) the current canonical source binding,
declared executable/input/result hashes, contract basis, or no-open-surprise
state differs from the handoff; (2) the complete suite has any failure, error,
skip, or fewer than the declared 37 distinct tests; (3) old intact recovery,
stale end checkpoint, and artifact-tampered recovery do not separate as
required; (4) same-HEAD candidate or canonical-integrated byte mutation is not
rejected before verdict/promotion; (5) the added verifier integration route
allows owner overlap, source drift, or an open surprise; (6) the actual launch
record lacks a real session, successful `stop`, matching fresh checkpoint,
zero return, or source-before/source-after equality. Required branch/state
exposures are valid-old/tampered/stale recovery; candidate/canonical-integrated
same-HEAD mutation; verifier verification/integration entry versus owner,
source-drift, and surprise negative controls; and real launch record versus
fake-process unit simulation. No RNG/stateful game workload is in contract, so
RNG accounting is inapplicable rather than assumed satisfied.

Pre-execution observations: all three recorded surprises are resolved;
canonical and paired-worktree HEADs equal the pinned commits, while canonical
trees are intentionally dirty and paired launch trees are clean. Candidate
source binding is distinct from the canonical evidence binding and will not be
substituted. The R8 correction invalidated the prior formal verdict; its new
evidence claims 37 tests. Next: checkpoint this plan, then independently
rehash/revalidate and run the full suite plus held-out negative controls.

## Fresh reproduction results — run-cb15199f9272fe496bd10a8a

Canonical `source-binding controls-bootstrap` produced the attached evidence's
engine digest `ccd8e02083e8d2e2b3e97976ace2273c8f924dfc02a39e919004eaf3544c50fd`
and RE digest `6696fd5201e144843617cbf6d78b41b5287ad5dcc9fa1e8aaa861d52b64e72e8`.
`campaign.py validate controls-bootstrap` passed. Independent byte hashes of
the two declared binaries, three declared inputs, and outcome package all
exactly match the contract. The package has 37 unique expected and 37 unique
passed method names, with no missing or extra names, return code zero and
`status: passed`.

`PYTHONDONTWRITEBYTECODE=1 python3 -m unittest discover -s verify/campaign
-p 'test_*.py' -v` reproduced **37/37**, zero skips/errors/failures, in 7.049
seconds. The independent held-out negative-control rerun of old recovery,
same-HEAD verdict/promotion drift, canonical integrated RE mutation, and final
integrated-verifier guards reproduced **4/4** in 1.093 seconds. Thus every
defined control branch exposed by these tests behaved as predicted; no failed
prediction was observed.

Independent parsing of the actual non-fake run record found 24/24 JSONL events,
zero error events, one completed/observed actual session, return code zero, a
`step_finish` reason `stop`, source-before equal source-after, and the matching
checkpoint session. Its observed model remains `unavailable`; it is an actual
Astra architecture-review launch, **not** a direct Terra normal-worker
execution. This is a residual/provenance limitation, not evidence of a Terra
execution, but does not falsify the narrowly worded unit-test criterion.

Decision: record a fresh scoped passing verifier verdict for the exact current
nonintegrated evidence only. Do not claim integrated acceptance, whole-engine
behavior, original comparison, replacement, replay, or game RNG/state
coverage. Exact next action: lead may attach a source-bound integrated package,
after which a fresh independent verdict must bind its changed evidence digest.

Actor `controls-independent-verifier`; role `verifier`; model
`openai/gpt-5.6-terra`; session `controls-independent-20260909-formal-1`.

## Scope and pre-execution falsifiers

This is a source-bound verdict only for `controls-bootstrap` criterion
`controls-negative-paths`, not engine, assets, research replacement, or an integrated package.
The verdict would fail if the attached artifact/binary/input hashes or either canonical source
manifest differed; if the suite had a failure, skip, or fewer than 36 tests; if old recovery
accepted corrupted artifacts or rejected solely for age; if a same-HEAD byte change did not
invalidate verdict/promotion; or if the purported normal launch lacked a real session, stop,
fresh matching checkpoint, zero return, or unchanged paired-worktree state. Required distinct
states were intact-old versus stale-end versus tampered recovery, candidate-engine versus
integrated-RE same-HEAD mutation, and real normal launch versus fake-process unit simulation.

## Independent observations and reproduction

Read `AGENTS.md`, `campaign/README.md`, contract
`campaign/contracts/controls-bootstrap.json`, current checkpoint
`campaign/runtime/checkpoints/controls-bootstrap-243f539b3219e74f12ef0db7.json`, raw evidence,
raw run JSON/JSONL/stderr, and Astra review `campaign/rollout/independent-review.md`.

`python3 tools/campaign.py --state-root /home/alex/sots-re source-binding controls-bootstrap`
recomputed engine `7741d42fc5e4e761e6449bdaf0e4a61d00036a23` digest
`ccd8e02083e8d2e2b3e97976ace2273c8f924dfc02a39e919004eaf3544c50fd` and RE
`3bfde5a70d874a723e797a695bbd847fd82c0aa7` digest
`82fc34631b2baa2ee74557020f74d68cc4db3c031561210f9933a3f22d7ff7b6`, exactly matching
the attached evidence. Independently rehashed all declared binaries, inputs, and result artifact;
each matched its declared SHA-256. `campaign.py validate controls-bootstrap` passed.

`PYTHONDONTWRITEBYTECODE=1 python3 -m unittest discover -s verify/campaign -p 'test_*.py' -v`
ran **36 tests**, all passed, zero skips, in 6.720 s. Held-out focused rerun:
`python3 -m unittest -v verify.campaign.test_controls.Controls.test_old_recovery_checks_integrity_but_not_age verify.campaign.test_controls.Controls.test_same_head_source_mutation_rejects_verdict_and_promotion verify.campaign.test_controls.Controls.test_integrated_re_source_mutation_rejects_acceptance`
ran 3/3 pass (0.722 s). The inspected tests require an old intact checkpoint to launch but reject
its stale end-checkpoint use and a post-checkpoint artifact modification; they alter candidate
engine and canonical RE bytes without changing HEAD and require source-content rejection before
verdict/integration/acceptance.

The actual, non-fake normal-launch record
`campaign/runtime/runs/run-df1472c13f31db3a4d5361f0.json` hashes to
`65dd1c1286742cd4d2401af5a229d7d014f60dd329dadee0dee78c499f61d663`.
Its JSONL has 24 parseable events, exactly one actual session
`ses_f77cf5062ffeTknrMfnbJMmdNh`, a `step_finish` with reason `stop`, return code 0, zero error
events, matching launcher checkpoint/session, and `source_before == source_after` for both paired
worktrees. Raw stderr is empty. Observed model is correctly `unavailable`, not fabricated; this
is an actual Astra architecture-review smoke, not evidence of a Terra worker launch.

## Decision and residual

Pass is justified only for the one declared controls test criterion and the exact nonintegrated
binding above. Astra R8 remains a separately recorded residual: the current launcher permits a
verifier in `verification` but not `integration`; it prevents the later fresh integrated-verifier
launch and requires Astra resolution. It neither converts this reproduced nonintegrated suite into
whole-engine acceptance nor is hidden as success. Exact next action: lead resolves R8, attaches
an integrated controls package, then obtains a new independent verdict over its changed digest.