fix(verify): fail closed on unsupported safety invariants (ARN-213)

[rita-aga]

Objective

Make unsupported safety-invariant expressions a hard verification failure instead of allowing a specification to pass with warnings.

Tracks ARN-213.

Current branch state

This draft opens immediately with ADR 0171, which defines the fail-closed capability boundary and structured source diagnostics. The mandated isolated RED regression and GREEN implementation will follow as separate commits.

Tradeoff

Specifications using invariant syntax that the verification backends cannot prove will be rejected at the deployment gate. This intentionally replaces warning-only acceptance; supported safety guarantees remain available, and unsupported forms must be modeled explicitly before deployment.

Validation plan

• Behavioral RED regression committed alone and demonstrated failing before the fix
• Focused verifier/spec/CLI tests
• Live CLI verification E2E before and after
• cargo fmt --check, git diff --check, strict clippy for touched crates, cargo test --workspace
• Fresh GPT-5.6 open-PR diff review to PASS, followed by Greptile

Do not merge: ARN-165 arena submission.

Greptile Summary

This PR makes unsupported safety invariants fail closed across verification and runtime paths. The main changes are:

• Structured capability diagnostics for unsupported invariant expressions.
• Runtime invariant metadata in transition tables and verification results.
• Actor replay, mutation, read, snapshot, and passivation checks for runtime safety contracts.
• Deployment, bootstrap, registry, CLI, and observe updates to preserve warnings and errors.

Confidence Score: 4/5

The hotswap safety-contract path needs a fix before merging.

• String state initial changes can bypass the migration gate.
• The rest of the fail-closed verification and runtime enforcement paths look consistently guarded in the changed code.

crates/temper-server/src/registry/model_contract.rs

Important Files Changed

Filename	Overview
crates/temper-server/src/registry/model_contract.rs	Adds model safety contract compatibility checks for hotswap, but omits string state initials from the migration decision.
crates/temper-server/src/entity_actor/actor.rs	Adds runtime safety checks during replay, reads, deletes, snapshots, and passivation.
crates/temper-server/src/entity_actor/effects.rs	Adds declared state initialization, field synchronization, and runtime invariant evaluation around action effects.
crates/temper-verify/src/diagnostic.rs	Adds structured unsupported-invariant diagnostics with source spans.
crates/temper-jit/src/table/types.rs	Extends transition tables with state initial values, runtime invariants, and model-protected state variables.

Prompt To Fix All With AI

Fix the following 1 code review issue. Work through them one at a time, proposing concise fixes.

---

### Issue 1 of 1
crates/temper-server/src/registry/model_contract.rs:128
**String Initials Bypass Migration**

When a hot-swap changes a string state variable's initial value while leaving the invariant text unchanged, this compatibility check ignores that state variable. The swap can pass even though the new `TransitionTable` initializes future actors with different string data, so an unchanged runtime invariant such as `title != ''` can start failing for newly spawned entities without the migration gate firing.

_{Reviews (1): Last reviewed commit: "fix(safety): close runtime enforcement r..." | Re-trigger Greptile}

Greptile also left 1 inline comment on this PR.

Context used (6)

• Context used - CLAUDE.md (source)
• Context used - AGENTS.md (source)
• Knowledge Base — temper-server
• Knowledge Base — Temper spec format, codegen, and verification
• Knowledge Base — Temper Runtime and Actor Runtime
• Knowledge Base — Temper WASM Runtime

[rita-aga]

Independent GPT-5.6 review of the open GitHub diff at 9ebbf338bb75751a6f9f56bd26a10fbe7083f9e1.

1. [P1] A runtime-invalid initial entity is still published and projected as created. EntityActor::GetState now returns an EntityResponse { success: false, ... } when a first action must establish an active runtime invariant, but ServerState::get_or_create_tenant_entity does not check response.success after the ask. It unconditionally emits the Created observe/SSE event and calls upsert_projection with the invalid state. That contradicts the PR's guarantee that the transient invalid shell is unreadable and never exposed: collection/query-plane consumers can discover it even though the direct actor response says creation failed. Return before all creation side effects when the response is unsuccessful (and clean up the newly indexed actor if appropriate), then add a server-level create/query regression—not only the direct actor test.

2. [P1] Production and deterministic simulation implement opposite initialization contracts. Production pre_start deliberately permits a zero-event state that violates a runtime invariant so an initializing action can repair it; EntityActorHandler::init instead immediately returns an error for the same state. Consequently DST cannot simulate the action-backed initialization lifecycle that production accepts, despite the ADR/readiness claim that runtime-enforced forms use the same evaluator and handler path. Choose one lifecycle contract and make both paths identical; if action-backed initialization remains supported, simulation needs the same non-durable/unreadable shell followed by the initializing action, with a regression covering equivalent production and simulation outcomes.

Verdict: FAIL

[rita-aga]

Remediated the independent-review findings from #391 (comment) in commit da2a371: failed pristine creation now exits before SSE/query projection and is removed from collection discovery; the first successful initializing action restores collection visibility; successful transitions to Deleted remove the ID instead of reindexing it; simulation now follows the same action-backed initialization contract. Focused HTTP and simulation regressions are rerunning on the pushed head.

[rita-aga]

Independent GPT-5.6 review of the open GitHub diff at da2a37168bdf77e51fb4e8ef337b426cebe89f8a.

The previous simulation/production initialization mismatch is resolved: EntityActorHandler::init now builds the same pristine state without rejecting it, and the regression drives the initializing action through the shared action path.

1. [P1] The initialization visibility fix still leaks runtime-invalid state to concurrent reads. get_or_spawn_tenant_actor_with_fields inserts the provisional entity ID into entity_index immediately after spawning (entity_ops.rs:760-768), before get_or_create_tenant_entity asks GetState and removes the ID on an unsuccessful response (entity_ops.rs:964-979). During that window, a direct OData GET passes entity_exists; load_existing_entity_body ignores response.success and serializes response.state (odata/read.rs:237-253). Collection fallback has the same problem: materialize_entity_set_entities treats every Ok(response) as visible, can upsert the invalid state into the durable query projection, and returns it (odata/read_support.rs:300-343). The added HTTP regression is sequential after POST completion, so it cannot catch this race. This violates the safety contract that the transient shell remains unreadable/unprojected until its initializing action succeeds. Do not publish provisional IDs, or make all read/materialization paths reject unsuccessful EntityResponse values (and add a deterministic concurrent create/read regression).

Current GitHub checks are still running; the completed verification, compile/lint, integrity, and platform-random jobs pass. The finding above is independent of those pending results.

Verdict: FAIL

[rita-aga]

Remediated the current-head publication race from #391 (comment) in commit 50869c6. Generic actor spawn no longer publishes collection visibility; validated create/action success is now the single publication boundary, with Deleted results removed. The regression explicitly spawns the pristine actor, performs a direct OData GET at that pre-validation interleaving, and requires 404 before the existing create/Issue flow proves post-initialization visibility.

[rita-aga]

Independent GPT-5.6 review of the open GitHub diff at 50869c61882d94ae31d7911ce7d68ba844c38b8a.

1. [P1] Delaying every index insertion until a successful create/action response hides valid, durable entities when the first action is rejected. get_or_spawn_tenant_actor_with_fields no longer publishes any ID, while EntityActor::pre_start still persists a bootstrap Created event whenever the pristine state satisfies its runtime invariants. dispatch_typed then calls update_entity_index_visibility only when the attempted action returns success = true. Therefore, spawning a valid entity followed by a guard/transition rejection leaves a real non-tombstoned journal entry permanently absent from collection discovery. The current GitHub DST/Platform Tests (platform-random) check reproduces this in the no-fault seed 0 workload: BudgetLedger:e-3 has 1 non-tombstoned events but is not in index. Publication needs to distinguish a runtime-invalid transient shell from a valid bootstrap-created state, including rejected-first-action paths; add a regression for that exact interleaving.

2. [P1] Direct actor simulation still silently accepts some verifier-unsupported declarations. EntityActorHandler::with_ioa_invariants validates only boolean references. Its translate_parsed maps CounterPositive, CounterCompare, NeverState, and trigger states without checking that the referenced counter/status is declared. SimActorSystem::evaluate_spec_assert then returns true for every non-items CounterPositive, so an invariant such as ghost > 0 becomes a passing simulated assertion even though the model builder correctly classifies the undeclared counter as Unverifiable/TVE001; an undeclared when state is similarly never triggered. This contradicts the ADR and readiness gate that direct backend entry points retain an unsupported sentinel and fail closed when the cascade is bypassed. Reuse the same declaration/type validation as the model builder and add direct-simulation regressions for undeclared counter and status references.

Current checks at review time: compile/lint, integrity, instrumentation, spec verification, and verification-contract checks pass; DST/Platform Tests (platform-random) fails as above; the remaining test shards are still running.

Verdict: FAIL

[rita-aga]

Remediated both findings from #391 (comment) in f512ffd. Publication now occurs at the actor response boundary when either the mutation succeeded (including no-journal actors) or prior durable sequence exists (including valid bootstrap + rejected first action); rejected zero-event shells remain hidden. Unsupported-safety classification now shares one declaration/type/capability contract across temper-spec, temper-verify, runtime artifact compilation, and direct simulation. Missing named counters fail closed, unsupported assertions trigger even with invalid when states, and direct regressions cover undeclared ghost > 0 plus undeclared trigger state. Exact CI seed replay: TEMPER_DST_RANDOM_MODE=smoke ... cargo test -p temper-server --test dst_platform_random dst_random_workload_no_faults -- --nocapture => 1 passed; direct-sim regression => 1 passed.

[rita-aga]

Independent GPT-5.6 final review of the open GitHub diff at f512ffdba7aa59841138300fc05cbfa33db63e87.

1. [P1] Live registry admission still bypasses the unsupported-invariant capability gate. The new preflight is applied in temper-platform deploy/bootstrap, but SpecRegistry::try_register_tenant_with_reactions_and_constraints still parses each IOA and immediately builds/swaps its TransitionTable without calling the capability classifier. This is a real activation path: temper-cli/src/serve/loader.rs::load_into_registry calls it directly, and persistent registry restore also registers specs before the platform bootstrap path. VerificationStatus::Pending does not prevent the table from becoming live. An unsupported assertion is therefore omitted from runtime_invariants and can execute unchecked when the server is started from a specs directory or restores an older persisted spec. The new hot-swap guard does not close this: it compares only compiled runtime contracts, so an unsupported incoming assertion and a model-only current spec both compare as an empty runtime-invariant vector and the unsafe table is swapped in. Put the shared declaration/type/capability preflight at the registry activation boundary (or prove every registration/restore caller gates before mutation), and add first-registration, restore, and hot-swap regressions.

2. [P1] No-journal passivation reopens the invalid-shell read leak after successful initialization. A successful initializing action without an event journal is now correctly published by update_entity_index_visibility, but its sequence_nr remains zero and its state exists only in the actor. passivate_idle_actors deliberately keeps the entity-index entry, takes no snapshot when there is no journal, and stops the actor. The next read respawns it with empty initial fields, recreating the runtime-invalid pristine shell. load_existing_entity_body checks only the retained index entry and then serializes the failed GetState response without checking response.success; collection materialization likewise treats every Ok(response) as visible. Thus an initialized no-journal entity becomes invalid yet remains discoverable after ordinary idle passivation, and direct/collection reads expose the shell. Preserve or remove visibility when passivating non-durable actors and make every read/materialization path reject unsuccessful responses; add an initialize → passivate → keyed/collection-read regression.

CI at review time is not green: Compile & Lint failed in cargo clippy --workspace --all-targets (exit 101); several test shards are still running. The completed verification-contract, integrity/DST, instrumentation, spec-verification, and platform-random checks pass.

Verdict: FAIL

[rita-aga]

Independent GPT-5.6 review of the open GitHub diff at 0fca3ec1c8bd21d923634deae407b61ad8a798f4.

The earlier publication, initialization, passivation, hydration-eviction, registry, replay-parameter, and callback-stack remediations are present. Two safety gaps remain:

1. [P1] The legacy production server constructors still activate unsupported invariants fail-open. ServerState::with_specs in crates/temper-server/src/state/mod.rs:842-856 builds every legacy table through TransitionTable::try_from_ioa_source. That builder in crates/temper-jit/src/table/builder.rs:24-27 only parses and then calls from_automaton; it does not call unsupported_safety_invariant_names, while from_automaton merely omits unknown assertions from runtime_invariants. with_persistence and with_storage_stack inherit this path, and check_verification_gate explicitly allows a tenant absent from SpecRegistry. Therefore a source containing assert = "used_bytes ** quota_limit" can still become a live server table and execute with no TVE001 and no runtime check. The new registry preflight does not cover this activation boundary. Apply the same dependency-light capability gate in the JIT fallible builder or every production constructor, and add legacy in-memory plus persisted-constructor regressions.

2. [P1] Newly synchronized action/PATCH values can violate model-proved boolean and literal-counter invariants. sync_declared_state_vars in crates/temper-server/src/entity_actor/effects.rs:229-269 copies every declared counter and boolean from caller values. It is called for action params before effects and for direct UpdateFields. The only post-mutation runtime gate, runtime_invariant_failure at effects.rs:611, evaluates table.runtime_invariants, which contains only StringNonEmpty and counter-to-counter forms. Model-proved BoolRequired, CounterPositive, and counter-to-literal assertions are absent. For example, a verified entity in an active state with invariant payment_captured can accept a direct update or otherwise legal action carrying {"payment_captured": false}; the new sync changes logical boolean state, the explicit effects need not restore it, and the action is persisted because the runtime invariant vector is empty. The same applies to items > 0 with {"items": 0}. Either keep caller field synchronization from mutating model state outside modeled effects, or evaluate the full supported invariant IR on every such mutation and replay; add action, PATCH, rollback, and replay regressions.

Focused corpus validation passes: 110 specs, 120 declarations, 120 typed. At review time GitHub compile/lint, verification contract, integrity/DST, spec verification, instrumentation, and platform-random checks pass; core, platform-boot, platform-consistency, and Tests remain pending.

Verdict: FAIL

[nerdsane]

Remediation for the current-head independent review FAIL at #391 (comment) is now pushed in 2df8ef3 (on top of af9b5d6).

Addressed all findings and the push-gate compatibility regression:

• all legacy ServerState constructors now reject unsupported safety invariants before registry activation
• model-protected counter/bool state cannot be implicitly overwritten by create/action params or PATCH/PUT; explicit modeled effects still work
• replay and snapshot hydration bind protected state to the serialized TransitionTable safety contract, validate checksum and sequence, and reset before authoritative full replay
• obsolete but structurally valid, identity-matching snapshots preserve only unprotected durable data and terminal Deleted state; malformed snapshots cannot inject data/status
• strict journal-read and concurrency retry paths fail closed without double-applying effects

Validation on current head:

• cargo fmt --check: PASS
• strict all-target/all-feature clippy: PASS
• git diff --check: PASS
• code review marker: PASS
• DST review marker: PASS
• cargo test --workspace (pre-push): PASS, including temper-server 680/680 and all standalone DST/integration/doc tests

Awaiting a fresh independent GitHub-diff review on current head before any Greptile request.

[nerdsane]

Independent GPT-5.6 review of the open GitHub diff at 2df8ef3a2a6c8aeec599ba9fbf90f7af8591804b.

The prior registry-admission, invalid-shell publication/passivation, production/simulation initialization, legacy-constructor, direct protected-variable mutation, and snapshot/replay blockers are materially addressed in the current diff. One safety gap remains:

1. [P1] Model protection is not closed over the state variables on which a proof depends. model_protected_state_var_names in crates/temper-spec/src/automaton/runtime_assert.rs:116-153 protects only counter/bool names that occur directly in CounterPositive, CounterCompare, or BoolRequired assertion nodes; it explicitly collects nothing for state-based properties such as NeverState, and it never includes variables used only by transition guards. build_initial_entity_state in crates/temper-server/src/entity_actor/effects.rs:129-170 and direct synchronization in effects.rs:267-304 therefore still allow callers to overwrite those unprotected logical counters/booleans through create fields or PATCH. This can invalidate the reachability assumptions under which a model invariant was proved. For example, with safe = true, unlock = false, an action guarded by is_true unlock whose modeled effect sets safe = false, and invariant safe, the verifier can prove the invariant because the action is unreachable. A create/PATCH carrying unlock = true is accepted because unlock is not in the invariant AST; the guarded action then executes its explicit modeled effect and persists safe = false. The post-action check at effects.rs:661-692 evaluates only runtime_invariants, so it does not catch the violated model-proved boolean invariant. The same issue applies to never(State) when an injected guard variable enables the forbidden transition. Protect every externally mutable model-state variable, or compute and enforce the full guard/effect dependency closure for each model-proved property, then add create and PATCH regressions that enable a previously unreachable invariant-breaking action and verify live execution plus replay remain inside the proved state space.

At review time Compile & Lint, Integrity/DST, Verification Contract, Spec Verification, Instrumentation, and platform-random pass; core, platform-boot, platform-consistency, and Tests remain pending. This finding is independent of those pending checks.

Verdict: FAIL

[nerdsane]

ARN-213 live local E2E — current head da5431dcdf25551e7f1f0edf6340d2b468810e03

Built binary: target/debug/temper

Unsupported registry admission fails closed

Fixture change (temporary E2E copy only):

[[invariant]]
name = "UnsupportedRegistrySafety"
when = ["Draft"]
assert = "ghost ** quota"

Exact command:

$ env TURSO_URL=file:/tmp/arn213-e2e/unsupported.db target/debug/temper serve --port 18131 --storage turso --specs-dir /tmp/arn213-e2e/unsupported --tenant arn213-unsupported --no-observe
  Storage: turso (file:/tmp/arn213-e2e/unsupported.db)
  Loading app: arn213-unsupported from /tmp/arn213-e2e/unsupported
    Loaded spec: Order (verification pending, lint clean)
Error: Failed to register tenant 'arn213-unsupported'

Caused by:
    cannot activate IOA for tenant 'arn213-unsupported', entity 'Order': unsupported safety invariants: UnsupportedRegistrySafety
$ echo $?
1

Supported registry boots and serves health

Exact commands and output:

$ env TURSO_URL=file:/tmp/arn213-e2e/supported-live.db target/debug/temper serve --port 18132 --storage turso --specs-dir /tmp/arn213-e2e/supported --tenant arn213-supported --no-observe
  Storage: turso (file:/tmp/arn213-e2e/supported-live.db)
  Loading app: arn213-supported from /tmp/arn213-e2e/supported
    Loaded spec: Order (verification pending, lint clean)
Starting Temper platform server...
  Temper Data API: http://localhost:18132/tdata
  App: arn213-supported (/tmp/arn213-e2e/supported)
  Verification: running in background (observe UI will stream progress)
  [verify] Order: [PASS] L0 Symbolic PASSED: 11 guards satisfiable, 5 invariants inductive, 0 unreachable
  [verify] Order: [PASS] L1 Model Check PASSED: 24 states explored, all properties hold
  [verify] Order: [PASS] L2 Simulation PASSED: 5 seeds, 43 transitions, 0 dropped msgs
  [verify] Order: [PASS] L3 Property Tests PASSED: 100 cases, 30 max steps
  [verify] Order: all levels passed

$ curl -sS -i http://127.0.0.1:18132/healthz
HTTP/1.1 200 OK
content-length: 0
date: Sat, 18 Jul 2026 19:26:42 GMT

The server was stopped with Ctrl-C after the successful request.

Contributor gate

This PR touches crates/temper-actor-runtime; outside-contributor sign-off is required before merge. This arena task will not merge the PR.

[nerdsane]

Independent GPT-5.6 review of the complete open GitHub diff at da5431d.

The current head closes the original guard-only injection for newly constructed actors: model-proved invariants now protect every declared boolean/counter, and the regression covers create, PATCH, action, and replay. One live-registry admission gap remains.

1. [P1] Model-safety contract changes can still hot-swap onto incompatible live and durable state. crates/temper-server/src/registry/mod.rs:187-208 blocks a migration only when compile_runtime_invariants changes. A model-proved invariant changes model_protected_state_vars (crates/temper-spec/src/automaton/runtime_assert.rs:119-138; compiled into the table at crates/temper-jit/src/table/builder.rs:163-164), but both the old and new runtime-invariant vectors can remain empty, so registry/mod.rs:267-278 swaps the new table into the same lock held by existing actors without validating their state. For example, an old invariant-free spec can accept unlock=true through PATCH; a subsequently verified spec can add invariant safe plus an action guarded by unlock that sets safe=false. The model proves that action unreachable from its declared initial state, but the registry admits the table over the live unlock=true actor, and effects.rs:593/661-693 checks only runtime_invariants, so the action can persist safe=false. Passivation can then snapshot that state under the new table contract. Extend the migration preflight to cover the model-proved safety contract as well as RuntimeInvariant (including invariant declarations/protection semantics), or validate and migrate every live/durable entity atomically before swap. Add an old-state -> verified guard-only hot-swap regression that proves rejection leaves the prior CSDL/source/table untouched.

All live GitHub checks for this exact head are green; this finding is independent of CI.

Verdict: FAIL

[rita-aga]

ARN-213 current-head remediation evidence

GitHub head: c05c4b1767f8994c9bc59d363fe8a341ef317bf3

Remediation commits since the prior independent FAIL:

• f60a193c — gate model-contract hot swaps
• d5aa6df0 — split registry model contract
• d608e698 — preserve verified hot-swap semantics
• c05c4b17 — preserve verified additive actions

The current head closes the live-registry admission gap and preserves fail-closed behavior across registration, startup restore, and hot swap. Model compatibility now compares invariant signatures, states/actions, and every resolved effect field/variant; safe additive actions are restricted to unique effect-free transitions from existing nonterminal states. Recursive terminal-leaf detection covers compound assertions. Durability coverage includes pre/post-swap journal restart replay and deterministic forced snapshot-failure retention.

Exact final push command:

git push -u origin HEAD

Final local gate result:

Gate 1/4: rustfmt check
Gate 2/4: cargo clippy
Gate 3/4: Readability ratchet
Gate 4/4: Full test suite
...
test result: ok. 694 passed; 0 failed
test result: ok. 6 passed; 0 failed  # dst_hotswap
test result: ok. 7 passed; 0 failed  # dst_platform_random (914.39s)
test result: ok. 4 passed; 0 failed  # dst_platform_rollback
test result: ok. 11 passed; 0 failed # e2e_gepa_loop
test result: ok. 6 passed; 0 failed  # wasm_dispatch
Pre-push: ALL GATES PASSED
To https://github.com/nerdsane/temper.git
   da5431dc..c05c4b17  HEAD -> codex/arn-213-unsupported-safety-invariants

The isolated rerun of the one load-sensitive WASM restore timeout from the preceding attempt passed 1/1; it then passed 6/6 in the final full gate without a code change.

Fresh independent GitHub-head review is now in progress. Greptile has not been requested yet, preserving the required gate order.

[rita-aga]

Independent review of the full current GitHub PR diff.

Reviewed head SHA: c05c4b1

Blocking finding:

[P1] Model-proved counter safety can still be mutated by effects omitted from the model. In crates/temper-spec/src/automaton/translate.rs:100-113, ResolvedEffect::is_verifiable excludes SetCounterFromParam, IncrementCounterByParam, and DecrementCounterByParam. crates/temper-verify/src/model/builder.rs:83-97 consequently removes those effects from every verification transition, and lines 148-157 explicitly classify them as runtime-only. However, the new model-protection contract in crates/temper-spec/src/automaton/runtime_assert.rs:110-139 treats counter-to-literal assertions as model-proved and says protected values change only through modeled transition effects. Production still executes SetCounterFromParam at crates/temper-server/src/entity_actor/effects.rs:882-905, while runtime_invariant_failure only evaluates the new StringNonEmpty and CounterVarCompare runtime subset. Therefore a spec with budget initially 0, an input action that sets budget from a parameter, and invariant budget <= 10 can pass the cascade because the model sees a no-op, then accept budget=100 live and durably replay it with no invariant rejection. The added test modeled_effect_can_consume_protected_action_param_during_replay demonstrates that this unmodeled effect is intentionally allowed through the protection boundary, but it only uses a safe value and does not test the false-proof case. Exact hot-swap effect comparison does not repair this initial admission unsoundness.

Please either model parameter-driven counter effects conservatively, reject them as a verification capability error whenever they can affect a model-proved claim or reachability, or atomically enforce the affected model invariant at runtime. Add a regression that proves cascade admission, live execution, and replay cannot accept an out-of-range parameter value.

I also traced unsupported-invariant preflight through cached/bootstrap/registry activation, runtime-contract rollback/publication, snapshot and journal hydration, contract-preserving hot swaps, additive action checks, and terminal-invariant handling. No additional blocking finding was identified in those scoped paths.

Verdict: FAIL

[nerdsane]

ARN-213 current-head validation and live E2E evidence

GitHub head: 971580793fddeccaae7b8fab359f14b16ffd3d2f

Full unbypassed push gate

Exact command:

cd /Users/seshendranalla/Development/temper/agent-worktrees/arn165/codex-arn-213-unsupported-safety-invariants
export CARGO_INCREMENTAL=0; git push -u origin HEAD

Exact terminal result:

Pre-push: ALL GATES PASSED
To https://github.com/nerdsane/temper.git
   c05c4b17..97158079  HEAD -> codex/arn-213-unsupported-safety-invariants
branch 'codex/arn-213-unsupported-safety-invariants' set up to track 'origin/codex/arn-213-unsupported-safety-invariants'.

The unbypassed hook ran cargo fmt --check, strict workspace Clippy, the blocking readability ratchet, cargo test --workspace, all server/platform DST suites, storage suites, and doctests. Notable durability stages included:

dst_platform_random: 7 passed; 0 failed (2598.55s)
dst_platform_rollback: 4 passed; 0 failed (145.43s)
e2e_gepa_loop: 11 passed; 0 failed
temper-server lib: 695 passed; 0 failed
Pre-push: ALL GATES PASSED

Behavioral RED/GREEN evidence

RED commit e60a495f before the fix:

cargo test -p temper-server --all-features --lib parameter_counter_effect_cannot_escape_verified_limit_live_or_on_replay -- --nocapture

unsafe live mutation must be rejected
test result: FAILED. 0 passed; 1 failed

Current-head GREEN:

test result: ok. 1 passed; 0 failed

Compatibility/dependency regressions:

cargo test -p temper-cli accepts_model_only_counter_invariant_on_postgres_actor_runtime -- --nocapture
test result: ok. 1 passed; 0 failed

CARGO_INCREMENTAL=0 cargo test -p temper-cli bootstrap_installed_apps_replays_persisted_app_when_registry_specs_are_stale -- --nocapture
Restored app 'temper-fs' for 'bootstrap-drift': Directory, File, FileVersion, Workspace
test result: ok. 1 passed; 0 failed

CARGO_INCREMENTAL=0 cargo test -p temper-spec runtime_assert::tests -- --nocapture
test result: ok. 10 passed; 0 failed

Live local startup E2E

The exact live startup commands and full output are preserved in the earlier E2E evidence comment. Observed behavior:

unsupported spec startup: exit status 1
cannot activate IOA ... unsupported safety invariants: UnsupportedRegistrySafety

supported control startup: verification cascade L0-L3 passed
GET /healthz: HTTP 200

The current full gate revalidated the same startup/registry capability path and the new parameter-derived live/replay path at exact head 97158079.

Review markers

Final local code-quality review: PASS, zero findings.

Final DST review: PASS, zero change-specific findings.

The PR-wide diff touches crates/temper-actor-runtime; outside-contributor sign-off remains required and flagged. The final ARN-213 parameter-safety remediation commits do not modify that crate.

[nerdsane]

Independent GPT-5.6 review of the full open GitHub PR diff.

Reviewed head SHA: 971580793fddeccaae7b8fab359f14b16ffd3d2f

1. [P1] The parameter/terminal capability rule is not wired into the verification cascade, so verification can still report a false pass for a contract that registry admission calls unsupported. crates/temper-spec/src/automaton/runtime_assert.rs:151-164 newly rejects an invariant when parameter-controlled counter semantics affect no_further_transitions, but crates/temper-verify/src/diagnostic.rs:27-31 and crates/temper-verify/src/cascade.rs:247-264 inspect only InvariantKind::Unverifiable from the older model builder; crates/temper-verify/src/model/builder.rs:202-233 never calls the new dependency classifier. A counterexample is a parameter-set budget, a Done -> Done action guarded by budget >= 2, and when = ["Done"], assert = "safe || no_further_transitions" with safe = false: the finite model drops the parameter assignment, keeps the guarded action disabled, and can pass every backend, while the real parameter value enables the forbidden transition. Registry activation eventually rejects it, but the public cascade, verify-ioa, and cached verification preflight can still claim success instead of returning TVE001 before any backend. Move the dependency-aware check into canonical verification classification and add a cascade regression for this OR/terminal case.

2. [P2] Parameter-derived runtime contracts are omitted from runtime-enforcement disclosures. compile_runtime_invariants attaches model-shaped counter, bool, and never assertions when parameter effects or guards require runtime enforcement (crates/temper-spec/src/automaton/runtime_assert.rs:84-113), but crates/temper-verify/src/diagnostic.rs:38-57 warns only when the model kind itself is RuntimeEnforced. Thus budget <= 10 compiled for runtime enforcement because of set_counter_from_param gets no warning in either a fresh cascade or cached deploy path. Derive disclosures from the compiled runtime contract, or carry dual model/runtime ownership in the IR, and cover the parameter-derived cached path.

Focused validation on this exact detached head: cargo test -p temper-spec runtime_assert::tests -- --nocapture passed 10/10, confirming the new classifier itself; the missing integration is between that classifier and temper-verify.

Verdict: FAIL

[nerdsane]

Fresh independent GPT-5.6 review of the open GitHub diff.

Reviewed SHA: 0c36145

Blocking finding:

• [P1] The public production source-to-JIT constructors still admit unsupported safety invariants. In builder.rs lines 24-27, TransitionTable::try_from_ioa_source only parses and then calls from_automaton. In lines 163-164, from_automaton uses compile_runtime_invariants, whose filtering contract omits unsupported declarations. Therefore TransitionTable::try_from_ioa_source returns Ok for a spec such as assert = "used_bytes ** quota_limit"; the resulting table carries no runtime invariant and can execute actions as though the safety claim did not exist. This is especially significant because the API documentation explicitly recommends the fallible constructor for production. Registry and platform callers added their own preflights, but the shared public source constructor remains a fail-open admission path, and direct JIT consumers (including the production WASM spec evaluator pattern) can bypass TVE001 entirely. Add the shared unsupported-safety preflight to the fallible source constructor (and ensure the infallible wrapper cannot silently compile such a table), or replace production-facing construction with a checked API and cover it with a regression asserting unsupported source cannot produce a TransitionTable.

The remaining reviewed paths are coherent: verifier backends fail closed at zero budget; cached and fresh deployment paths preserve capability checks and runtime-only disclosures; declaration/source-span matching is exact and ordered; runtime-only assertions are checked on tentative state with rollback; snapshot contract binding, full replay validation, tombstones, passivation, and hot-swap rejection address the durability/replay boundary. Several GitHub CI jobs were still pending at review time, while Verification Contract, Integrity/DST Patterns, and Spec Verification had passed.

Verdict: FAIL

[rita-aga]

Fresh independent GPT-5.6 review of the OPEN GitHub PR diff.

Reviewed exact GitHub head: ace07b4ec4eca856ac462cbbfb441ae225710d97

PR state verified: open, unmerged.

Findings: no actionable correctness, durability, regression, or DST findings on the current diff.

Review notes:

• Unsupported safety declarations fail closed in the canonical verifier preflight, registry admission, and public JIT constructors; structured TVE001 diagnostics retain exact source spans.
• Runtime-only and parameter-derived enforcement contracts are disclosed consistently through fresh, cached/bootstrap, CLI, registry, persistence, and Observe result paths.
• Parameter-driven counter effects now reject missing, malformed, negative, and out-of-range values atomically across live execution, replay, and deterministic simulation, while preserving established numeric-string compatibility for increment/decrement amounts.
• Tentative runtime-invariant failures roll back state before persistence; snapshot contract binding, full-journal fallback, replay validation, tombstone handling, passivation, and hot-swap migration gates preserve durable safety boundaries.
• Unsupported simulation invariants are recorded at actor registration, so zero-tick/dropped-message runs cannot false-pass.
• Runtime enforcement artifacts and documentation consistently use contract version 2.
• Determinism-sensitive changes use ordered collections and simulated time/UUID sources; no change-specific wall-clock, nondeterministic iteration, thread, filesystem, or network dependency was introduced.
• The outside-contributor sign-off flag for crates/temper-actor-runtime remains a separate merge gate; this review does not authorize merging.

Per reviewer-session constraints, I reviewed GitHub-hosted metadata, changed-file patches, and exact-head file contents and did not edit, build, test, or create a worktree.

Verdict: PASS

[rita-aga]

@greptile review

[rita-aga]

ARN-213 final exact-head E2E and validation evidence

GitHub head: acfd7c4336a7a6241bdaf860e8349fd25f2cbdaa

Full unbypassed push gate

Exact command:

CARGO_INCREMENTAL=0 git push -u origin HEAD

Terminal result:

Gate 1/4: rustfmt check
Gate 2/4: cargo clippy
Gate 3/4: Readability ratchet
Gate 4/4: Full test suite
...
temper-server: 699 passed; 0 failed
randomized platform sweep: 7 passed; 0 failed (1414.74s)
rollback: 4 passed; 0 failed
GEPA: 11 passed; 0 failed
Pre-push: ALL GATES PASSED
To https://github.com/nerdsane/temper.git
   ace07b4e..acfd7c43  HEAD -> codex/arn-213-unsupported-safety-invariants

Greptile remediation regression

CARGO_INCREMENTAL=0 cargo test -p temper-server registry::model_contract_tests -- --nocapture

test registry::model_contract_tests::hot_swap_rejects_string_initial_change_under_runtime_invariant ... ok
test result: ok. 5 passed; 0 failed

This proves a string-initial change under an unchanged safety invariant is rejected before registry mutation and preserves the prior source, swap-controller identity, and live table.

Live unsupported startup: fails closed

TURSO_URL=file:/tmp/arn213-e2e-ace07b4e/unsupported-acfd7c43.db target/debug/temper serve --no-observe --specs-dir /tmp/arn213-e2e-ace07b4e/unsupported --tenant arn213-final --port 3215

Loaded spec: Order (verification pending, lint clean)
Error: Failed to register tenant `arn213-final`
Caused by:
    cannot activate IOA for tenant `arn213-final`, entity `Order`: unsupported safety invariants: UnsupportedRegistrySafety
exit status: 1

Live supported control: starts and serves health

TURSO_URL=file:/tmp/arn213-e2e-ace07b4e/supported-acfd7c43.db target/debug/temper serve --no-observe --specs-dir /tmp/arn213-e2e-ace07b4e/supported --tenant arn213-final --port 3216
curl -sS -i http://127.0.0.1:3216/healthz

[verify] Order: [PASS] L0 Symbolic PASSED: 11 guards satisfiable, 5 invariants inductive, 0 unreachable
[verify] Order: [PASS] L1 Model Check PASSED: 24 states explored, all properties hold
[verify] Order: [PASS] L2 Simulation PASSED: 5 seeds, 43 transitions, 0 dropped msgs
[verify] Order: [PASS] L3 Property Tests PASSED: 100 cases, 30 max steps
[verify] Order: all levels passed

HTTP/1.1 200 OK
content-length: 0
date: Mon, 20 Jul 2026 19:32:14 GMT

The live server was stopped with Ctrl-C after the successful request.

Contributor gate

This PR touches crates/temper-actor-runtime; outside-contributor sign-off remains required before merge. This arena task will not merge the PR.

[rita-aga]

Independent GPT-5.6 final review of the complete open GitHub PR diff at acfd7c4336a7a6241bdaf860e8349fd25f2cbdaa.

No actionable findings.

• The unsupported-safety capability gate is consistently represented across parsing, verification diagnostics, JIT construction, registry admission, bootstrap, production handling, simulation, persistence, hydration, and replay. Unsupported declarations fail closed; supported runtime assertions are type checked and rolled back before persistence on violation.
• Publication, passivation, reconstruction, snapshot compatibility, and event replay paths preserve the validated safety contract and reject malformed or contract-mismatched durable state without exposing an invalid entity shell.
• The Greptile string-initial migration finding is fully remediated in acfd7c43: hot-swap compatibility now includes string initial values whenever a safety invariant exists, while invariant-free specs retain unrestricted ordinary swap behavior and the existing safe metadata/additive extension cases remain accepted. The regression verifies atomic rejection and preservation of the prior source, swap-controller identity, and serialized live table.
• The changed simulation-visible code uses deterministic containers and simulated time, introduces no new thread, ambient filesystem/network, random, or nondeterministic iteration dependency, and exercises invariant, rollback, replay, passivation, hot-swap, and randomized DST cases.
• PR fix(verify): fail closed on unsupported safety invariants (ARN-213) #391 is OPEN and unmerged at this exact head. The crates/temper-actor-runtime outside-contributor sign-off remains a separate merge gate; this verdict does not authorize merging.

Verdict: PASS

[rita-aga]

ARENA SHIPPABLE · GPT-5.6 · 2026-07-20T19:50:13Z

Exact current GitHub head: acfd7c4336a7a6241bdaf860e8349fd25f2cbdaa

Mandatory gate audit, in order:

1. PR fix(verify): fail closed on unsupported safety invariants (ARN-213) #391 is open and unmerged.
2. Pre-Greptile independent exact-head PASS: fix(verify): fail closed on unsupported safety invariants (ARN-213) #391 (comment)
3. Greptile request, posted only after that PASS: fix(verify): fail closed on unsupported safety invariants (ARN-213) #391 (comment)
4. Greptile completed with one actionable P1 thread. Remediation commit: acfd7c4
5. Concrete remediation reply and resolved thread: fix(verify): fail closed on unsupported safety invariants (ARN-213) #391 (comment)
6. Fresh final independent review on remediated exact head, Verdict: PASS: fix(verify): fail closed on unsupported safety invariants (ARN-213) #391 (comment)
7. Final exact-head live E2E and complete local gate evidence: fix(verify): fail closed on unsupported safety invariants (ARN-213) #391 (comment)
8. Exact-head CI is fully green: https://github.com/nerdsane/temper/actions/runs/29772307177

Validation summary:

• CARGO_INCREMENTAL=0 git push -u origin HEAD: unbypassed pre-push pipeline PASS
• rustfmt, strict workspace Clippy, readability ratchet, full workspace tests, all DST/platform/storage suites, and doctests PASS
• temper-server 699/699
• randomized platform sweep 7/7
• rollback 4/4
• GEPA 11/11
• Greptile remediation model-contract tests 5/5
• live unsupported startup exits 1 with named unsupported invariant
• live supported control passes L0-L3 and returns HTTP 200 from /healthz

Thread-aware final audit: Greptile review completed; its sole actionable thread has a concrete diff/test reply and is resolved.

Contributor gate: this PR touches crates/temper-actor-runtime; outside-contributor sign-off remains required before merge. MERGE NOTHING — this arena task does not merge the PR.