Skip to content

fix(release): consolidate consequence-boundary hardening and evidence - #723

Merged
FutureEnterprises merged 63 commits into
mainfrom
codex/pr-queue-release-train
Sep 2, 2026
Merged

fix(release): consolidate consequence-boundary hardening and evidence#723
FutureEnterprises merged 63 commits into
mainfrom
codex/pr-queue-release-train

Conversation

@FutureEnterprises

@FutureEnterprises FutureEnterprises commented Sep 2, 2026

Copy link
Copy Markdown
Member

Outcome

Consolidates the exact head commits from #712, #713, #714, #715, #716, #717, #718, #721, #722, #708, and #685 against the current strict main base, then regenerates the shared content-addressed evidence once.

This also carries only the two generic hardening commits from #710: governed proof-run serialization and the AIUC incident-field schema check. The AIPS-1 P3 lab and insurer-specific/commercial composite are deliberately excluded from the public tree pending IP/FTO review.

Material reconciliation

  • Keeps executor authority bound to exact adapter inputs and native replay units.
  • Closes service, PR-kit, signoff-tenant, custody, encoder, and named-evidence fail-open paths.
  • Makes authoritative NOT_COMMITTED reconciliation terminal while allowing an idempotent read of the exact terminal row after a lost COMMIT response; it never reopens or deletes the authority row.
  • Preserves Stripe bank_account.change.default_for_currency through the verified actuator.
  • Applies standalone runtime rewrites on every render path and fixes the source layout that previously regenerated trailing whitespace.
  • Closes a Node/browser verifier split: both runtimes now refuse a valid Ed25519 signature carrying an unregistered algorithm label, and the public forgery corpus tests the hostile case in both paths.
  • Revalidates the AIC source lock against the current IETF identity-certificate draft and regenerates the deterministic report/evidence.
  • Preserves the distinction between verification, authorization, dispatch, provider outcome, and physical effect.

Exact-head evidence

  • Full test run: 10,489 passed, 181 skipped; 653 files passed, 13 skipped (10,670 cases / 666 files total).
  • Governed proof census: 20 Tamarin lemmas, 35 executable security claims, 335 conformance vectors, and 359 external hostility cases.
  • Security case: 35/35 executable claims passed; 261 evidence files hashed.
  • Formal synchronization: 14 models, 21 claims, 78 scenarios, 26 TLA invariants, and 13 composed lifecycle invariants.
  • Conformance: all 21 suites / 335 vectors passed across the labeled JS, Python, and Go same-team ports.
  • Production build, core typecheck, package-focused tests, clean-room v2, source-lock fetch, migration history, repository boundary, release chain, and npm audit --audit-level=high passed.

Two PostgreSQL-only named tests were skipped locally and are not represented as passes; GitHub's PostgreSQL integration/schema jobs remain release gates.

Operational boundary

The repository includes a pending migration, but this PR does not claim that migration has been applied to any live Supabase project. No provider response is treated as proof of physical effect.

Closes #722
Closes #721
Closes #718
Closes #717
Closes #716
Closes #715
Closes #714
Closes #713
Closes #712
Closes #708
Closes #685

FutureEnterprises and others added 30 commits September 1, 2026 04:02
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
…apters

Each finding was reproduced by an executed PoC against origin/main and
re-run after the fix.

E-1 (langchain, CRITICAL). The Proxy gated only `invoke`; every other
function was bound to the raw target, so langchain-core's `.call()`,
`.batch()` and `.stream()` (which reach the effect through `this.invoke`)
resolved to the ungated original. A PoC wired $1,000,000 through `.call()`
and $2,000,000 through `.batch()` with no receipt. `.call`, `.batch`,
`.stream`, `.func` and `._call` are now gated explicitly, and every other
method is bound to the receiver so an internal `this.invoke(...)` also
lands on the gate. Each entry point runs exactly once per authorized
action. The legacy `withGuard` proxy refuses on the same entry points.

E-2 (openai-guard, CRITICAL). The documented simple form
`action: 'payment.release'` was not argument-bound, so one receipt for that
action authorized any arguments: a PoC spent a receipt approved for
$100 -> acct_OK on $9,999,999 -> acct_ATTACKER. `bindToolAction` is now
applied unconditionally, exactly as the langchain and openai-agents
adapters do; `actionFor` may only refine the base action type. The digest
also now covers the arguments that actually execute (the `__ep` receipt
envelope is stripped before hashing, not after).

E-read-3 (openai-agents). `action` was not destructured out of `opts` and
the gate options were spread after it, so a caller-supplied `opts.action`
replaced the derived argument-bound action: one receipt for an arbitrary
string approved every tool and every argument set while the returned
decision still reported the derived action. `action` is discarded and the
gate options are spread first, matching packages/langgraph.

E-read-4 (crewai). A signed `expires_at` was never enforced, so with
`max_age_sec=None` a receipt that expired 30 days ago still ran, and a
`verify_assurance` callback returning a bare string was trusted as ok.
`expires_at` is now an absolute bound (fail-closed when unparseable),
mirroring packages/require-receipt, and only `{"ok": True, "tier": ...}`
or the literal `True` satisfies the assurance check.

Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
…ders canonical

Seven confirmed red-team findings. Each was reproduced against the shipped
code before the change and re-run after.

A-1 (HIGH) lib/grace/reference-adapters.ts:50 createFencedMemoryStore()
returned { durable: true, ownershipFenced: true } over a process-local Map.
lib/grace/mobile-grid.ts runCurtailmentOnce gates the physical grid dispatch
on exactly those two booleans, and lib/grace/reference-scenario.ts wired the
store straight into it. Two pods each held their own Map, so one idempotency
key produced two curtailment dispatches. The store is now
createEphemeralMemoryStore() and reports durable/ownershipFenced/
permanentConsumption as false, matching MemoryConsumptionStore in
packages/gate/src/store.ts. runCurtailmentOnce additionally requires
permanentConsumption, so a TTL-reopening store cannot dispatch twice either.

A-2 (HIGH) lib/grace/curtailment.ts runSettlementOnce is the money path and
its docstring promised to "atomically reserve across a fleet", but it only
checked that reserve and commit were functions. Two pods each paid out once
for a single {entitlement_id, event_id, meter_window_digest}. Both boundaries
now share one predicate, isGraceCustodyStore (durable + ownershipFenced +
permanentConsumption), with named refusals settlement_store_custody_insufficient
and execution_store_custody_insufficient. executeGraceCurtailment checks both
stores BEFORE dispatching, so a settlement store that cannot hold custody
refuses the run instead of surfacing after the physical curtailment fired.
The demo harnesses (reference scenario, refinement adapter) pass an explicit
allowEphemeralState: true, which executeGraceCurtailment refuses outright when
NODE_ENV is production, and createGraceReferenceRuntime now throws there.

C-1 packages/verify/src/pq-signature-agility.ts b64urlToBytes decoded without
a round-trip check. Buffer ignores the slack bits in the final base64url
character, so each 64-byte Ed25519 signature had four accepted spellings that
all verified: a signed artifact's bytes were malleable without touching the
signature. Exactly one encoding per byte string is accepted now, matching the
receipt path. lib/signatures.ts BASE64_RE likewise admitted a mixed +/ and -_
alphabet before normalizing; a value must now be entirely standard base64 or
entirely base64url, with padding that matches the body length.

C-2 packages/verify/src/receipt-cose-encoding.ts built decoded maps with
object[key] = val, so a "__proto__" text key hit Object.prototype's accessor:
a string value was silently dropped and an object value replaced the decoded
object's prototype. Two distinct deterministic CBOR inputs decoded to one
canonical value, falsifying the round-trip claim behind
conformance/encoding-equivalence/vectors.json. Object.defineProperty writes an
own data property for any key, so decode is lossless (matching JSON.parse) and
no prototype is reachable from input.

C-5 The same decoder accepted major type 1 with arg 2^53-1, decoding to
-9007199254740992, while the encoder refuses that value. The decoder's domain
was wider than the encoder's; it now refuses with unsupported_item.

C-4 signature.algorithm is not covered by the signature and was only checked
for presence, so a receipt labelled "ML-DSA-65" or "none" carrying a valid
Ed25519 signature came back valid:true in JS, Go and Python, and other modules
branch on that label. All three verifiers now require the label to name the one
algorithm EP-RECEIPT-v1 defines. Both shipped spellings of that name are
accepted: production issuers and all 425 conformance vectors emit "Ed25519",
while the published spec text (docs/trust-receipt-spec.md,
app/spec/trust-receipt/page.tsx) and the cross-language fixtures show
"ed25519". No shipped vector carries any other value; verified by scanning
every conformance/**/*.json for a receipt-shaped signature.algorithm.

C-3 lib/create-receipt.ts derived its idempotency key as
sha256(`${submitter.id}:${transactionRef}:${transactionType}`). ':' is legal
inside both a ref and a type, so {ref:'inv-9:refund', type:'settlement'} and
{ref:'inv-9', type:'refund:settlement'} produced one key and the second
submission was silently handed the first one's receipt with deduplicated:true.
The target entity was not an input at all, so the same submission about two
different entities collapsed to one key. The key is now derived after entity
resolution over length-prefixed, NUL-joined fields including the resolved
target entity id (the discipline lib/agent-mailbox.ts and
lib/works/demand-service.ts already use), under a versioned ep_idem2_ prefix so
a new key can never collide with a v1 key already stored.

Tests: custody predicate and both GRACE boundaries (tests/grace-curtailment,
tests/grace-mobile-grid, including the production refusals); non-canonical
base64url signature and key spellings (packages/verify/pq-signature-agility);
both __proto__ cases and the negative-integer bound
(tests/receipt-cose-encoding); the algorithm label in all three runtimes
(packages/verify/test.js, packages/go-verify/verify_test.go,
packages/python-verify/tests/test_verify.py); the mixed-alphabet, slack-bit and
padding refusals (tests/signatures); the collision pair and the cross-entity
key (tests/receipt-idempotency).

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
…ayer

Each item below was found by reading the code, then reproduced by a test that
fails on origin/main before the fix.

1. consequence-actuator readiness and bind
   runtime.ts ready() returned 200 when config.readiness was not a function
   (the field is optional at the config interface), so the startup gate in
   server.ts, which only checks `status !== 200`, passed vacuously for a config
   that had proved nothing about its durable dependencies. Readiness is now a
   proof: no probe means 503 with `readiness_probe_not_configured`, a refusing
   probe means `readiness_probe_refused`, a throwing probe means
   `readiness_probe_failed`. server.ts also bound `environment.HOST ||
   '0.0.0.0'` while both sibling services use `?? '127.0.0.1'`, and `||` turned
   HOST='' into a bind on every interface. Bind now defaults to loopback
   through a validated listenSettings(), matching gate-service/src/server.ts and
   consequence-control-service/src/server.ts. Every deployment path already sets
   HOST=0.0.0.0 explicitly (Dockerfile.consequence-actuator:21,
   deploy/consequence-control-cloud-run/deploy.sh:99), so the default change
   does not alter how the service is actually deployed.

2. consequence-control provider-evidence envelope binding
   github-app.ts checked nonce, envelope_digest and provider_attribution_digest
   only `if (expected.X !== undefined)`. The sole production caller builds
   `expected` from the nine reconciliation keys
   (packages/gate/src/proposal-to-effect.ts:1020), so those three never ran at
   all -- and they are exactly what ties an observation to ONE execution
   envelope. A directly presented, correctly signed COMMITTED observation from
   another envelope of the same attempt was accepted. All three are now
   required, refused as `provider_evidence_envelope_binding_absent` when the
   caller pins none and `provider_evidence_binding_mismatch` when they differ,
   matching the exactKeys() discipline of the reconciliation branch.

3. consequence-control expired proposals on the mutating routes
   Four of six lifecycle routes passed { allowExpired: true } to the controller.
   pollApproval and lookupAttempt are read-only and keep it, now documented.
   reconcile and repairAeb mutate durable AEB state and had NO time bound at
   all. They are now bounded by a recovery window: a proposal may still converge
   an already-made attempt for a fixed window past expires_at, then the route
   refuses with `proposal_recovery_window_elapsed`, and a proposal with no
   parseable expiry is refused outright.

4. trust-receipt execution attestation drift
   The reject branch fired only when execution_binding.required === true.
   Otherwise a re-derived hash mismatch was written as
   `guard.trust_receipt.executed` with binding_status 'drift' and answered 201
   with a logger.warn -- an audit trail reading "executed" for an action that is
   not the action the receipt authorized, and not the `execution_drift_refused`
   check this project publishes in
   public/.well-known/agent-action-control.json. A mismatch is now always a
   refusal: 409 `execution_action_drift` (hash) or `execution_binding_mismatch`
   (observed high-risk fields), with the drift recorded as evidence first.

5. /api/v1/guarded consumption and action validation
   The failed-commit branch released the reservation while its own comment said
   the reservation blocks replay; the release re-opened exactly that window, so
   the next request with the same receipt was allowed. The reservation is now
   kept. lib/http/guarded-consumption.ts passed ttlSeconds: 900, which sets
   permanentConsumption:false and advertises a 900s retention, but the Supabase
   backend inserts only (consume_key, state), writes no expiry, and nothing
   reaps: the claim described a reaper that does not exist. Consumption is now
   declared permanent, which is what the storage actually does. `action` came
   off an unvalidated query parameter and was interpolated into the
   WWW-Authenticate header and the consumption key; it is now validated against
   a closed identifier pattern before any use, refused as `action_invalid` with
   no challenge header on that path. On auth: this route stays a PUBLIC
   REFERENCE endpoint, and the code now says so -- it performs no privileged
   effect and mutates no business state; a 200 means "this receipt would have
   authorized this action", not that anything ran.

6. gate-service pinned human-assurance inputs
   config.ts made approverKeys, rpId and allowedOrigins optional whenever a
   verifyAssurance function was supplied, so a config module could substitute
   `() => true` and start the service with nothing pinned to verify against.
   The pins are required unconditionally now: a custom verifier may change how
   they are checked, never whether they exist. No caller in the tree supplies
   verifyAssurance, so nothing in the repository loses a configuration.

7. OIDC login tenant oracle
   app/api/sso/oidc/login/route.ts answered with a distinct status and a
   tenant-echoing detail per case, letting an unauthenticated caller enumerate
   the tenant namespace. Unified to one status and one generic body across
   unknown tenant, unconfigured tenant, and config-store failure, matching
   app/api/sso/saml/acs/route.ts.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
The manifest hashes the verifier source trees, and the custody plus encoder
fixes changed them. Suite and vector counts are unchanged (21 suites, 332
vectors, 3 one-team ports).

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
…the wrapper

The AEB adapter contract says the replay unit is verifier-derived from the
native authority: the same authority under a different wrapper is one unit,
distinct authorities are distinct units, and a field the mapping profile
declares non-material can never be its sole discriminator. Four adapters
broke that rule, and each break is either a double consume or a permanent
denial of a valid authority.

B-1 (HIGH) OAuth transaction-challenge keyed the unit on access_token.jti,
which the shipped profile itself declares non-material. A second access
token for one AS transaction produced a second unit, so both operations
reached AUTHORIZED through evaluateAebEvidence and authorizeAebExecution on
one shared store. The unit is now {protocol, authorization_server, audience,
transaction}, matching the WIMSE OAuth adapter.

B-2 (HIGH) CCS v1.3 keyed on {source, issuer, nonce} while declaring nonce
non-material. Two distinct authorities that reused one nonce collided onto
one unit and the second was permanently denied; one authority re-issued
under a fresh nonce split into a second consumable unit. The unit is now
{source, issuer, audience, action}, where action is
"ccs:tool-invoke:<tool>:<sha256 of the canonical arguments>", covered by the
Ed25519 signature and cross-checked against tool and params_hash. CCS-L1 had
the same inconsistency and now keys on {source, issuer, audience,
public_key_fingerprint, action, tool, args_digest}. The public draft-08 v1.3
Crossing Lab example adapter carried the same derivation and is fixed the
same way.

B-3 (MEDIUM) The McGraw delegation adapter keyed on a digest of the raw
artifact bytes while accepting COSE_Sign1 both tagged and untagged. The CBOR
tag sits outside Sig_structure, so one signed proof yielded two units. The
unit now keys on the untagged signed form (Sig_structure plus signature).
B-3b: the adapter computed evidence_digest over the decoded bytes while the
evaluator computes it over the artifact string and hard fails on mismatch,
so every McGraw leg was malformed_native_result. The adapter now uses the
evaluator's convention; the evaluator is unchanged.

B-4 (MEDIUM) The Crossing Lab replay row varied only artifact_ref, which no
wrapper-keyed adapter can fail. Workspaces may now supply an optional
replay_probe carrying a second valid native encoding of the same authority
and a distinct authority. Both are pin-checked and refused if vacuous, and
they produce two rows: the re-presented authority must land on one unit, the
distinct authority on its own. The generated sample workspace supplies the
probe, and the sample native protocol now carries presentation_id outside
its signature so the probe has something real to exercise.

Evidence: the six red-team PoCs flip from exploited to refused; new tests in
each adapter fail against the pre-fix derivation and pass after; the
Crossing Lab probe is proven by mutating the sample adapter to key on
presentation_id and on nothing. Conformance report references regenerated
for the changed units.

Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
…inding floor

Four confirmed red-team findings in the adoption template and the manifest
floor behind it.

E-3 (critical) receipt-required-pr-kit: a tool that did not resolve to a
manifest entry ran with no gate at all. `delete_all_records_v2`,
`drop_database`, and the case-mismatched `DELETE_ALL_RECORDS` all executed.
`findActionRequirement` also returns null for an ambiguous or conflicting
resolution, which the kit collapsed into "safe, proceed". dispatch() now
refuses unless the manifest resolves the tool to exactly one entry, names the
case-sensitivity near-miss explicitly, and treats ambiguous/conflict as a
refusal. This is the posture mcp-guard already takes with
defaultIrreversible = true.

E-4 (high) the gate bound only `{ target: args?.table }` while executing the
full, still-mutable `args` object, and a call with no `table` degraded to the
bare action type. Arguments are now snapshotted before the first await,
bound with bindToolAction over the whole call, and the snapshot is what
executes.

E-5 (high) the template exported its own Class-A proof minter and honoured
EMILIA_ALLOW_INLINE_KEY unconditionally. The demo approver key and minter
moved to demo-approver.ts, which is imported only in demo mode and refuses to
load under NODE_ENV=production; the inline-key escape is ignored there too.
The per-action gate memoization, which contradicted the "read at call time"
comment, is gone; consumption is now one process-wide store.

E-6 (high) validateActionRiskManifest never required execution_binding, and
verifyExecutionBinding returns ok on an empty field list, so a legacy
EP-ACTION-RISK-MANIFEST-v0.1 receipt_required action was bound to the action
TYPE alone. A receipt signed for $1.00 to acct_OK executed $999,999.99 to
acct_ATTACKER through the Stripe adapter, manifest validating clean. The
validator now requires non-empty execution_binding.required_fields on every
guarded entry, and the Gate binds the canonical observed action for a legacy
entry that declares none, so a manifest loaded without re-validation still
fails closed.

Fixtures that constructed guarded manifests without execution_binding now
declare the material fields they observe; no assertion was relaxed. The
shipped .well-known manifest, the COSA example, the audit demo, the JSON
schema, and the MCP guide were updated for the same floor.

Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
…ff reads to the tenant, fail closed by default

Assurance (F-4). scripts/verify-security-case.mts checked only that a claim's
named test title appeared in the file, and executePlannedTests ran the whole
file and recorded result "passed" for every planned title. Emptying the body of
a named evidence test (title preserved) left --validate-only reporting
METADATA OK and the file green.

- planTest now also requires the exactly titled test to have a callback body
  that executes something once comments are stripped.
- executePlannedTests now runs each file under a machine-readable reporter
  (vitest --reporter=json, node --test-reporter=tap), parses the per-test
  outcome, and fails the case when a planned title was never executed or did
  not pass. Runner-level skips are reported instead of being silently counted
  as evidence. One process per file keeps the runtime close to before.
- tests/security-case-evidence-binding.test.ts pins the static half.

Security (E-read-1). app/api/signoff/[challengeId]/route.ts looked a challenge
up by challenge_id alone and then accepted a global operator / signoff.view
permission with no tenant comparison, even though signoff_challenges carries
tenant_id (supabase/migrations/072). Cloud tenant keys now read through a
tenant-scoped lookup like app/api/cloud/signoff/escalate, and an untenanted
protocol-plane key can no longer read a tenant-owned challenge on the strength
of a global permission.

Fail-closed default (E-read-2). EP_AUTHORITY_ENFORCEMENT defaulted to 'shadow',
so the block branch in app/api/v1/trust-receipts/route.ts was dead, including
registry_unavailable and revoked_authority. The default is now
'enforce_default', an unrecognized value fails closed rather than observing,
and 'shadow' / 'warn' are documented as an explicit non-production opt-out.
Suites that mock Supabase with no registry pin the observe-only mode
themselves.

Mobile SDK. sdks/kotlin-mobile EmiliaMobileContinuity.retrySafe defaulted to
true and canDecideSafely treated an absent statement as safe, while the Swift
SDK defaults to false. Kotlin now matches: absent means not retry-safe.

Public claims. Replaced transcribed test/bundle numbers in DUE_DILIGENCE.md
with pointers to the generated files; corrected the AEC vector count, the
mutation figure, the three stale gate-suite totals, "best-in-class", and the
"independent"/"third-party" re-performance wording in docs/CAPABILITY-MAP.md;
renamed the synthetic assurance demo off a real firm's name; dropped the
unsupported "governed pilots" surface claim from the llm-context inputs;
scoped the README prevention line and the complete-mediation sentence; fixed
the Alloy fact range in formal/PROOF_STATUS.md.

security/security-case.json is reconciled to the new evidence-file hashes.

Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
…ndle

The two added regression suites move the measured test totals, and the
security-case evidence bundle changed with scripts/verify-security-case.mjs.
Regenerated with npm run sync:proof-stats (full --execute against the pinned
TLA2Tools 1.7.4 jar) and npm run sync:llm-context.

Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
typecheck:rest failed on the PR kit: `makeReceiptGate().run()` inferred
`ok: boolean`, so `if (r.ok)` narrowed nothing and `r.result` / `r.status` /
`r.body` were all errors on the union. The fix belongs in the gate, not at the
call site: `check()` and `run()` now declare
`ReceiptGateCheckResult` / `ReceiptGateRunResult`, whose `ok: true` / `ok:
false` members discriminate, and `run()` is generic over the effect's return so
`result` carries the caller's own type instead of `unknown`. The two-argument
`run(receipt, fn)` form resolves through a named type guard, because
`Record<string, any>` also admits callables and a bare `typeof` test narrowed
it to the structureless `Function`. No cast at any call site, and the emitted
.d.ts now carries the same discriminants for every consumer.

Re-emits the selected-scenario conformance source digests for the files this
branch changed.

Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
reconcileAebExecution and reconcileAebExecutionDurable returned
{ state: 'AVAILABLE', retry_allowed: true } on NOT_COMMITTED by deleting the
reservation, and proposal-to-effect mapped that to a terminal RELEASED attempt.
Because aebReservationKey is derived from the evaluation record (caid,
action_digest, operation_id, consumption_nonce), re-presenting the same
evaluation re-derived the byte-identical key and re-reserved it. One action
instance, one AEB one-time unit, four provider invocations in a loop.

draft-schrock-action-evidence-boundary-04 s5.11 forbids exactly that:
reconciliation must not resurrect the original authorization or silently
release its one-time replay unit, and a policy-permitted later attempt must
use a new action instance.

An authoritative NOT_COMMITTED now marks the reservation terminally
RELEASED_NOT_ENTERED. The key is never reservable again, the native replay
fences it installed stay installed, a late COMMITTED stays refused, and every
reconciliation result carries retry_requires_new_instance: true. A durable
store must declare terminalRelease and implement releaseTerminal(); without it
the durable path fails closed with terminal_release_unsupported rather than
degrading to the non-terminal release(). release() stays the abort primitive
for an attempt that provably never reached the provider.

The Postgres store keeps the row and marks it RELEASED_NOT_ENTERED through a
new security-definer release_terminal_operation, with an idempotent forward
migration for the state domain and the released_at column.

formal/ep_complete_mediation.tla gains the reservation lifecycle, a
ReconcileNotCommitted transition into the terminal state, the
ReleasedReservationNeverReReserved and InvocationRequiresReservedUnit
invariants, and a second deliberately unsafe control that hands the released
reservation back. TLC: safe model clean at 54 distinct states, both mutations
produce their expected counterexamples.

Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
…d reservation

Emitted by npm run security-case:emit. The
ambiguous-effect-is-never-auto-retried claim now covers ReserveOneTimeUnit,
ReconcileNotCommitted, and RefuseReReserveAfterRelease, plus the
ReleasedReservationNeverReReserved and InvocationRequiresReservedUnit
obligations.

Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
The DDL constant in packages/gate/src/aeb-consumption-store.ts is the audit
copy; production applies supabase/migrations. Without this migration
release_terminal_operation would not exist in a deployed schema and the durable
reconciliation path would fail closed on every authoritative NOT_COMMITTED.

Adds released_at, widens the state domain to RELEASED_NOT_ENTERED with a named
lifecycle constraint, and exposes an executor-scoped security-definer UPDATE
that keeps the row and its replay fences. Every step is idempotent. Registers
the file in supabase/migration-history.v1.json and adds the column to the live
schema contract.

Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
…odex/pr-queue-release-train

Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
…into codex/pr-queue-release-train

Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>

# Conflicts:
#	conformance/conformance-manifest.json
…odex/pr-queue-release-train

Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>

# Conflicts:
#	AI_CONTEXT.md
#	conformance/conformance-manifest.json
#	public/.well-known/emilia-context.json
#	public/llms-full.txt
…codex/pr-queue-release-train

Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>

# Conflicts:
#	AI_CONTEXT.md
#	lib/proof-stats.json
#	public/.well-known/emilia-context.json
#	public/llms-full.txt
#	public/llms.txt
#	security/security-case.json
…' into codex/pr-queue-release-train

Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>

# Conflicts:
#	AI_CONTEXT.md
#	DUE_DILIGENCE.md
#	conformance/conformance-manifest.json
#	lib/proof-stats.json
#	papers/preprint/main.tex
#	public/.well-known/emilia-context.json
#	public/llms-full.txt
#	public/llms.txt
#	security/security-case.json
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>

# Conflicts:
#	AI_CONTEXT.md
#	conformance/clean-room/v2/bundle.v2.json
#	conformance/conformance-manifest.json
#	docs/conformance/CLEAN-ROOM-V2.md
#	lib/proof-stats.json
#	papers/preprint/main.tex
#	public/.well-known/emilia-context.json
#	public/llms-full.txt
#	scripts/verify-clean-room-submission-v2.mjs
#	scripts/verify-clean-room-submission-v2.mts
#	security/security-case.json
#	tests/clean-room-v2.test.ts
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>

# Conflicts:
#	AI_CONTEXT.md
#	public/.well-known/emilia-context.json
#	public/llms-full.txt
#	public/llms.txt
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
(cherry picked from commit 8b2cd5f)
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
(cherry picked from commit a5b948c)
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>

# Conflicts:
#	AI_CONTEXT.md
#	conformance/clean-room/v2/bundle.v2.json
#	conformance/conformance-manifest.json
#	docs/conformance/CLEAN-ROOM-V2.md
#	lib/proof-stats.json
#	packages/verify/dist/index.d.ts.map
#	packages/verify/dist/index.js.map
#	papers/preprint/main.tex
#	public/.well-known/emilia-context.json
#	public/llms-full.txt
#	public/llms.txt
#	scripts/verify-clean-room-submission-v2.mjs
#	scripts/verify-clean-room-submission-v2.mts
#	security/security-case.json
#	tests/clean-room-v2.test.ts
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
@strix-security

strix-security Bot commented Sep 2, 2026

Copy link
Copy Markdown

Strix is installed on this repository, but we couldn't run this PR security review because this workspace's trial has ended. Add a card to resume code reviews here.

So far, Strix has reviewed 68 pull requests, surfaced 13 security issues (8 critical/high) and blocked 8 risky merges across this workspace.

@vercel

vercel Bot commented Sep 2, 2026

Copy link
Copy Markdown

The latest updates on your projects. Learn more about Vercel for GitHub.

Project Deployment Actions Updated
emilia-protocol Ready Ready Preview Sep 2, 2026 9:05am UTC

Request Review

Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
Signed-off-by: FutureEnterprises <team@emiliaprotocol.ai>
@FutureEnterprises
FutureEnterprises merged commit bd7022a into main Sep 2, 2026
73 checks passed
@FutureEnterprises
FutureEnterprises deleted the codex/pr-queue-release-train branch September 2, 2026 09:25
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant