23 Confidential and Verifiable AI Computation

23.1 Chapter status

Field	Value
Chapter ID	`confidential-and-verifiable-ai-computation`
Part	Part I - Foundations, Alignment, and Governance
Status	conceptual
Last updated	2026-08-01
Primary source records	`ext_nist_privacy_enhancing_cryptography_2026`, `ext_zkllm_2024`, `ext_ietf_rats_architecture_2023`
Claim label	Design rationale
Evidence level	argument
Source loading state	source notes: `ext_nist_privacy_enhancing_cryptography_2026`, `ext_zkllm_2024`, `ext_ietf_rats_architecture_2023`
Test state	The 31-declaration `AsiStackProofs.ProtectedComputationReview` model and independent 48-axis consumer pass locally; this mechanizes only the bounded protected-execution dossier, not cryptographic security, hardware trust, privacy, authorization, or acceptable deployment cost.

23.2 Drafting guardrail

Cryptographic and attestation terms remain scoped to named guarantees, adversaries, implementations, and evidence statements. No construction is presented as proof of semantic correctness, legitimate purpose, complete privacy, production security, or safe deployment.

23.3 Human Reading Path

Concrete lens. The enclave-only baseline treats valid attestation as end-to-end protection. The compositional contract includes fallback, metadata, purpose, authorization, leakage, and disclosure.

Use this layer to separate what protected computation establishes from properties that still require policy, custody, testing, and judgment. Privacy, Data Rights, and Information-Flow Governance establishes permitted information use. This material asks what parties can learn or verify when computation crosses a distrust boundary. Model-Weight Custody and Hardware Roots of Trust owns the keys, artifacts, measured platforms, and recovery authority.

Consider a transaction: a user wants prompt confidentiality, a provider wants weight confidentiality, and an auditor wants evidence that an approved artifact ran. Attestation identifies a measured environment without proving its policy legitimate. A zero-knowledge proof establishes an encoded relation even when that relation misstates intended meaning. Outputs, timing, access patterns, logs, caches, and fallback may still leak.

Name the adversary and assets, declare permitted leakage, choose a construction, state exactly what its evidence proves, and preserve revocation and observable failure. Compare protected execution with a competent simpler design under equal task, quality, context, concurrency, and lifecycle accounting. Treat encrypted, attested, proved, authorized, semantically correct, and private end to end as distinct claims requiring distinct evidence.

23.4 Problem

AI computation increasingly crosses distrust boundaries: a user may need to hide inputs, a provider may need to protect weights, an auditor may need to verify the executed artifact, and every party may need output integrity without granting another party unrestricted custody. Ordinary transport encryption ends before computation begins.

The requirements are often asymmetric and simultaneous. A hospital may trust its own data steward but not a cloud operator, while a model provider may trust neither the hospital nor the accelerator host with model weights. A regulator may need a verifiable statement without receiving either secret. Repeated queries, output content, timing, access patterns, caches, receipts, and failure behavior create additional leakage channels. A complete design must therefore state which party is protected from which observer, for which asset, during which lifecycle stage, and under which cryptographic or hardware assumptions.

23.5 Why existing approaches are insufficient

Privacy policy governs permitted information use, while hardware custody governs stored artifacts. Neither supplies a guarantee-by-guarantee execution contract covering input confidentiality, model confidentiality, computation integrity, output authenticity, attestation freshness, leakage, verifier policy, cost, and failure recovery.

Security adjectives make the gap worse. “Encrypted inference” may describe transport, selected tensor operations, or a fully protected execution path. “Attested” may identify a measured binary without validating its policy, inputs, dependencies, or output meaning. “Proved” may establish an arithmetic relation whose circuit mistranslates the intended computation. Benchmarking only successful, short requests can conceal concurrency collapse, key rotation, revocation, verifier disagreement, recovery cost, and silent fallback to an ordinary service precisely when protection fails. It can also omit setup amortization, parameter generation, dependency updates, side-channel review, and the burden of keeping historical receipts verifiable after keys, algorithms, platforms, and policies change.

23.5.1 Strongest objection

The strongest objection is that the proposed contract over-engineers a problem that ordinary access control, transport encryption, organizational separation, and contractual accountability can solve more cheaply. That objection often wins: if every relevant party and platform is inside one adequately governed trust domain, adding FHE, MPC, zero-knowledge proofs, or remote attestation can increase cost and failure surface without changing the actual decision risk. The compositional contract is still necessary because it makes that simpler baseline explicit and testable. Protected execution earns admission only when a named distrust boundary remains, its guarantee closes that boundary under a declared adversary, and the measured lifecycle benefit exceeds the new cryptographic, hardware, verifier, recovery, and leakage costs. Otherwise the system should retain the simpler governed route.

23.6 Core Claim

[confidential-and-verifiable-ai-computation.core, label: Design rationale, support: argument] Confidential and verifiable AI requires a compositional execution contract that names the adversary, protected assets, permitted leakage, trust anchors, proof or attestation statement, verifier policy, freshness, revocation, performance budget, and authorization boundary; no primitive or attestation may be treated as proof of semantic correctness, legitimate purpose, or end-to-end privacy.

Reader claim. An attested enclave can prove which code ran while the overall service still leaks through inputs, outputs, metadata, fallback, or an unauthorized purpose.

Operational rule. Compose confidentiality, integrity, proof statement, trust anchors, freshness, leakage channels, verifier policy, authorization, observable fallback, revocation, and cost at the transaction boundary. Reject any unprotected fallback unless separately authorized and disclosed; never let attestation imply semantic correctness or end-to-end privacy.

23.6.1 Worked protected computation: the enclave is valid, the fallback leaks

A service attests that the expected model code ran inside a protected environment and returns a valid proof about the encoded computation. Under load, the protected path exceeds its latency budget and silently falls back to an ordinary worker. The answer remains correct, but the prompt and intermediate state now cross a boundary the consumer did not authorize. The compositional contract rejects the transaction because fallback protection and disclosure are part of the guarantee, not operational trivia.

Even on the protected path, output length and timing may exceed the declared leakage allowance, and a valid attestation says nothing about whether the user’s purpose was legitimate. The finite review gives exact repair or refusal dispositions to 48 admission-axis mutations, tracks arbitrary leakage-channel lists, invalidates receipts under five scope changes, rejects two unprotected fallbacks, and preserves non-substitution between evidence types. It does not establish cryptographic soundness, hardware trust, side-channel resistance, leakage measurement, authorization, privacy, or acceptable cost.

23.7 Start with a guarantee vector, not a security adjective

Mechanism. Declare the adversary, protected assets, permitted leakage, trust assumptions, availability need, unsupported properties, and separate guarantees for inputs, weights, intermediates, execution, outputs, and audit before choosing technology. Failure mode. “Private” or “secure” can collapse mutually different confidentiality, integrity, authenticity, and authorization claims. Non-claim. A complete guarantee vector proves none of its entries. Source grounding. NIST’s privacy-enhancing cryptography program supplies distinct primitive families and composition pressure, not implementation assurance.

Suppose a hospital wants a model provider to process a record. “Run this securely” is underspecified. The hospital may want input confidentiality from the provider, the provider may want weight confidentiality from the hospital, both may want proof that an approved model and preprocessing pipeline ran, the patient may want purpose limitation, and an auditor may need enough evidence to reconstruct the transaction. Availability, output authenticity, deletion, and access-pattern leakage remain separate again.

The execution contract therefore begins with a vector:

Property	Question the contract must answer	Typical mechanism family	Residual boundary
Input confidentiality	Who can learn prompts, records, retrieved context, or features?	FHE, MPC, confidential execution, local computation	Outputs, access patterns, timing, and logs may still leak
Model confidentiality	Who can recover weights, adapters, system prompts, or proprietary preprocessing?	Confidential execution, MPC, ZK-compatible commitments, access control	Query extraction and output leakage remain
Computation integrity	Was the committed function evaluated on committed inputs?	ZK proofs, authenticated computation, replicated checks	A faithful computation can encode the wrong function
Platform identity	What code and configuration ran on what measured environment?	Remote attestation	The measured artifact and appraisal policy may be flawed
Output authenticity	Did this result come from the named transaction and artifact?	Signatures, commitments, authenticated channels	Authentic output need not be true or safe
Usage privacy	What is learned across repeated queries?	Differential privacy, rate limits, aggregation, query policy	Utility and group leakage remain
Availability and recovery	What happens when protected execution fails or becomes too slow?	Redundancy, explicit fallback, checkpointing, revocation	Silent downgrade can erase every other guarantee

This table prevents guarantee laundering. A trusted execution environment can conceal memory from some platform actors without proving the model’s semantic correctness. A zero-knowledge proof can establish an encoded relation without showing that the relation represents the intended policy. Fully homomorphic encryption can evaluate over ciphertext while leaving output release, key custody, purpose, and downstream use unresolved. NIST’s privacy-enhancing cryptography program is useful precisely because it treats FHE, MPC, zero-knowledge proofs, and related tools as different families that can be composed rather than as one magic privacy layer.

23.8 Pick a construction only after declaring the distrust boundary

Mechanism. Select local execution, confidential hardware, FHE, MPC, zero knowledge, differential privacy, private retrieval, or a hybrid by matching its trust and leakage model to the declared boundary. Failure mode. A fashionable primitive can protect the wrong asset, shift trust to an undeclared party, or compose into weaker end-to-end behavior. Non-claim. Construction selection is not a security proof or policy authorization. Source grounding. NIST provides family-level terminology; zkLLM is one configuration-bound proof-of-possibility comparator.

Mechanism selection is a systems decision, not a prestige ranking.

Local execution removes a network counterparty from the inference path but places model custody, device compromise, and resource constraints on the user side.
Confidential execution can protect data and weights from portions of a hosting stack and can release keys after a verifier accepts fresh attestation. Its trust base includes hardware, firmware, attestation roots, the measured software, and the appraisal policy.
FHE can keep selected inputs encrypted during computation, but supported operations, ciphertext expansion, approximation, memory traffic, and latency determine whether the workload is usable.
MPC distributes trust among parties and can protect collaborative computation if the corruption and communication assumptions hold. Network rounds, collusion thresholds, and availability are first-class costs.
Zero-knowledge proofs can let a prover convince a verifier that a committed relation holds without revealing protected witnesses. The circuit or arithmetic representation, setup assumptions, prover cost, and semantic correspondence remain part of the claim.
Differential privacy constrains what output distributions reveal about an individual’s contribution. It does not hide the raw input while an untrusted machine processes it.

Hybrids are normal. For example, an attested environment can protect a model and generate a signed inference receipt while a privacy mechanism limits released aggregates. But composition can also create new leakage. A receipt that binds a user, prompt hash, precise time, and model version may improve auditability while worsening linkability. Each composition needs one threat model and one end-to-end data-flow review, not a stack of disconnected vendor claims.

23.9 Evidence is a statement appraised by a party

Mechanism. Bind model, code, preprocessing, configuration, parameters, input and output commitments, platform state, and policy identity into the statement that is evidenced or proved. Failure mode. A valid proof can execute the wrong artifact or omit behavior performed outside the committed relation. Non-claim. Artifact binding does not establish model quality, output truth, or legitimate purpose. Source grounding. zkLLM motivates model and inference commitments within a bounded circuit; no general artifact-binding implementation is reproduced here.

The RATS architecture usefully separates an Attester, a Verifier, and a Relying Party. That separation belongs in the ASI stack. The machine producing evidence should not be allowed to declare that its own evidence is acceptable. The verifier evaluates evidence against reference values and an appraisal policy; the relying party decides what the resulting attestation result authorizes.

A protected AI transaction should bind at least:

the model, adapter, tokenizer, system policy, preprocessing, tool policy, and relevant runtime configuration;
input or data commitments appropriate to the privacy boundary;
platform and software measurements where hardware attestation is used;
a nonce, epoch, or challenge that prevents replay;
the verifier-policy identifier and reference-value version;
an output or output commitment, transaction identifier, and time window;
revocation and incident state.

Freshness matters because a valid statement about yesterday’s software is not evidence about today’s patched—or compromised—system. Reference values and verifier policies also change. A hash can remain identical while a certificate chain is revoked; a certificate can remain valid while the allowed model version has changed. Lifecycle state therefore belongs inside appraisal.

23.10 The circuit-to-semantics gap

Mechanism. Keep Attester, Target Environment, Attesting Environment, Verifier, Relying Party, endorsements, reference values, evidence, appraisal policy, and authorization action as separate identities and receipts. Failure mode. Collapsing roles lets a vendor assertion become its own independent authorization. Non-claim. An Attestation Result is not proof of trustworthy intent, semantic correctness, or verifier independence. Source grounding. RFC 9334 supplies this informational architecture; it is not a deployed protocol or local root-of-trust result.

zkLLM is an important proof of possibility: its authors report bounded zero-knowledge proofs for large-model inference with model privacy under their construction and configurations. The book should use that result for what it is—a research prototype demonstrating that some nontrivial inference relations can be proved—not as evidence that arbitrary production inference is now cheaply, privately, and semantically verified.

The verifier learns that the encoded arithmetic relation held. It still needs answers to harder questions:

Did the encoding match the published model architecture, numerical rules, tokenizer, sampling policy, and input transformation?
Were approximate operations and quantization bounded in a way that preserves the claimed behavior?
Did the proved output include every relevant tool call, retrieval, cache lookup, policy check, and postprocessor?
Was the committed model the model the user was authorized to query?
Does a correct execution produce a safe, truthful, or lawful answer?

These are not objections to proofs. They are the reason proof statements need precise names. “Inference relation (R) held for commitments (x), (w), and (y)” is strong and auditable. “The AI answer was verified” is usually too broad to be meaningful.

23.11 Cost and fallback are security properties

Mechanism. Bind freshness through nonce, timestamp, or epoch; record reference-value and policy versions; and make revocation, rotation, reappraisal, and replay rejection explicit. Failure mode. Stale evidence can remain cryptographically valid after firmware, artifact, workload, verifier policy, or compromise state changes. Non-claim. Fresh evidence does not establish current semantic correctness or lawful use. Source grounding. RATS provides freshness and appraisal distinctions; this chapter has produced no attestation evidence.

A protected path that works only for a tiny prompt or one user is not a deployment result. Native and protected runs must share task inputs, model quality, hardware accounting, batch policy, concurrency, context length, failure policy, and measured scope. Report prover and verifier time separately, peak memory, proof or evidence size, setup and key costs, throughput, tail latency, energy, and failed-transaction rate.

Cost can become a privacy and safety failure. Long queues reveal which transactions take unusual branches. Resource exhaustion can be a denial of service. Most dangerously, an operator may silently fall back to ordinary cloud inference. The contract must say whether failure causes rejection, reduced functionality, a different protected construction, or an explicitly authorized unprotected path. Users and downstream services must be able to tell which path produced the result.

23.12 Mechanism

Mechanism. Maintain a semantic correspondence review from intended operation through preprocessing, quantization, circuit or measured environment, committed inputs and outputs, and the consumer’s interpretation. Failure mode. The encoded relation may be satisfied exactly while implementing the wrong preprocessing, approximation, policy, or meaning. Non-claim. Reviewing correspondence does not prove equivalence for all inputs. Source grounding. zkLLM makes the configuration-bounded circuit relation concrete; its reported result does not close the circuit-to-semantics gap.

Express the requested guarantee vector separately for input privacy, model privacy, intermediate-state privacy, computation integrity, output authenticity, availability, and auditability.
Choose among FHE, MPC, zero-knowledge proofs, confidential execution, private retrieval, differential privacy, or hybrid composition against an explicit adversary and leakage model.
Bind code, model, configuration, data commitments, platform state, nonce or epoch, and policy identity into evidence that a distinct verifier appraises.
Keep cryptographic correctness, attested identity, model quality, semantic validity, user authorization, and lawful purpose as separate claim classes.
Measure native and protected execution with the same task, hardware accounting boundary, quality target, batching, concurrency, and failure policy.
Provide key rotation, algorithm agility, verifier-policy update, revocation, incident response, fallback, and artifact retirement.

flowchart LR
  D["Adversary, assets, and permitted leakage"] --> G["Guarantee vector"]
  G --> P["Primitive or trusted-compute path"]
  P --> C["Artifact, input, policy, and configuration commitments"]
  C --> V["Independent evidence appraisal"]
  V --> F{"Fresh, matching, and authorized?"}
  F -- "no" --> B["Block, revoke, recover, or request explicit fallback"]
  F -- "yes" --> O["Release bounded output and receipt"]
  O --> L["Leakage, cost, and incident monitoring"]
  L --> R{"Boundary or implementation changed?"}
  R -- "yes" --> D
  R -- "no" --> O

How to read this protected-execution loop: the distrust boundary determines a guarantee vector before a construction is selected. Commitments and independent appraisal release only a bounded statement; mismatch, staleness, or missing authority blocks the path. Leakage, cost, incidents, and change feed back into the contract instead of silently downgrading protection.

Composition is handled as an intersection of scoped statements, not as an accumulating security score. A confidential execution environment can protect runtime memory while a proof binds a selected computation and an authorization service governs key release. The resulting claim is no stronger than the interfaces joining them: artifact commitments, freshness, verifier policy, preprocessing identity, output release, and revocation must all refer to the same transaction.

Failure handling is part of the protection boundary. Timeouts, unsupported operators, memory pressure, verifier unavailability, and key-service failure must produce an observable state that downstream consumers can distinguish. An explicit fallback can be authorized for a narrower task, or the request can be rejected and recovered elsewhere. Quietly substituting an unprotected path would invalidate both the receipt and the user’s information-flow decision.

23.12.1 A protected-execution receipt

Mechanism. Account for outputs, access patterns, timing, memory traffic, failures, logs, caches, proofs, metadata, verifier queries, and composition with neighboring services as explicit leakage channels. Preserve the attacker’s observation surface and measurement method in the receipt rather than writing “encrypted” as a terminal verdict. Failure mode. Inputs or weights can remain hidden while outputs, repeated queries, page faults, timing, or operational metadata reveal protected information; a proof system can also enlarge denial-of-service or traffic-analysis surfaces. Non-claim. Enumerating leakage does not measure it, prove side-channel resistance, or establish end-to-end privacy. Source grounding. NIST warns that primitive families expose different leakage and trust assumptions, RATS notes sensitive evidence, and zkLLM reports bounded costs. None supplies a local side-channel evaluation, so this remains design rationale.

The reusable artifact is not a blanket security badge but a ProtectedExecutionReceipt:

request_id
guarantee_vector
adversary_and_leakage_model_id
artifact_and_configuration_commitments
platform_or_proof_statement
freshness_challenge_and_epoch
verifier_policy_and_reference_values
output_commitment
measured_cost_and_fallback_path
authorization_decision_reference
revocation_and_incident_state
unsupported_properties

The receipt can be public, selectively disclosed, or itself protected, depending on the linkage threat. Its job is to make the claim reconstructible. It must never contain raw secrets merely because the receipt is an audit artifact.

23.13 Interfaces

Privacy and Data Rights for consent, purpose limitation, retention, access, and remedy
Model-Weight Custody for key custody, artifact provenance, hardware roots of trust, and media sanitization
Security Kernel for identity, authorization, recovery, cryptographic agility, and fail-closed policy
Inference Systems for latency, batching, caching, paging, and cost accounting
Safety Cases for verifier independence and claim-bounded assurance

Each interface owns a different kind of truth. Privacy supplies permitted purpose and rights; custody supplies artifact and key identity; the kernel supplies authorization and recovery; inference supplies observed resource and quality behavior; assurance supplies appraisal and challenge. The protected execution record joins their identifiers without allowing one owner to certify another’s property or broaden the relying party’s conclusion. That separation also preserves independent challenge, appeal, and incident ownership. No owner becomes a universal security oracle.

23.14 Invariants

Every protected execution declares its adversary, assets, leakage, trust assumptions, freshness condition, and unsupported properties.
An attestation proves only the appraised statement about a measured environment; it does not prove trustworthy intent, correct policy, or correct output meaning.
A zero-knowledge proof proves only the encoded relation under its cryptographic assumptions; the circuit-to-semantics gap remains explicit.
Confidentiality mechanisms do not override consent, purpose, deletion, contestability, or downstream-use constraints.
Fallback from protected to unprotected execution requires explicit authorization and cannot occur silently.

These rules keep cryptographic validity subordinate to the complete transaction: the right artifact, policy, party, time, purpose, and fallback state must remain distinguishable even when every primitive functions as specified.

23.15 Failure modes

Mechanism. Compare protected and native paths under the same task, quality target, context, concurrency, hardware boundary, batching, failure policy, and total operator cost; authorize any downgrade separately and make it observable and expiring. Failure mode. An unusable protected path can silently fall back, or unmatched accounting can hide quality loss and verifier burden. Non-claim. Feasible latency does not prove security, and costly protection is not automatically safer. Source grounding. zkLLM supplies source-reported performance pressure; no local protected-execution benchmark has run.

Guarantee laundering collapses confidentiality, integrity, privacy, authorization, and correctness into one secure-compute label.
Stale or replayed attestation is accepted after artifact, platform, policy, or revocation state changed.
Side channels, outputs, access patterns, logs, caches, or failure timing leak protected information.
The proved computation faithfully executes the wrong model, wrong preprocessing, wrong policy, or semantically invalid relation.
Protected execution becomes unusable under realistic context, concurrency, memory, or latency and silently falls back.
Verifier, root-of-trust, key-management, or parameter-selection compromise invalidates the guarantee.

23.15.1 Strongest challenge and simpler baseline

The strongest challenge is that most deployments do not need advanced cryptography. A carefully isolated service with ordinary authenticated encryption, minimal logging, strict access control, short retention, and independent audit may be cheaper, easier to inspect, and safer than a complex protected-compute system. That is a real baseline, not a straw man.

The new layer earns admission only when the distrust boundary cannot be removed organizationally or locally, and when the chosen construction improves a named guarantee without unacceptable quality, reliability, or lifecycle cost. A construction that adds cryptographic sophistication but enlarges the trusted code base, prevents recovery, or obscures policy can be a regression.

23.16 Minimum Viable Implementation

A guarantee matrix and local demonstration for one bounded inference operation with explicit adversary and leakage models, artifact and configuration commitments, freshness, independent verification, native-versus-protected latency and cost accounting, negative tests for replay and mismatched artifacts, and a no-authorization non-claim.

The demonstration should run valid and invalid transactions through separately implemented prover or attester and verifier paths. Negative controls should change the model, tokenizer, preprocessing, policy, nonce, epoch, relying party, and fallback state; each mismatch must fail closed with a reconstructible reason. Measurements should include quality, latency, memory, concurrency, setup, verification, rotation, and recovery costs. The artifact would show a bounded contract and evidence flow, not production security, complete leakage resistance, or end-to-end privacy. The minimum record also preserves unsuccessful attempts and unresolved residuals.

23.17 Mature Research Target

A meaningful advance would make confidential and verifiable inference deployable as a substrate-independent contract, compare multiple trust and cryptographic constructions under a common workload, expose residual leakage and semantic gaps, and preserve audit, revocation, rollback, and purpose governance across the full lifecycle. The mature operational contract would make every downgrade observable and keep cryptographic evidence separate from authorization, semantic correctness, quality, and end-to-end privacy.

At that endpoint, one workload specification could exercise local execution, confidential hardware, multiparty computation, homomorphic computation, zero-knowledge verification, and hybrid paths without changing the claimed task or hiding different trust assumptions. Independent appraisers would reconstruct statements from receipts, inject stale roots and mismatched artifacts, inspect side channels, and measure failure recovery. Results would be reported by guarantee, adversary, context, concurrency, and lifecycle cost rather than as a universal secure-inference ranking. Long-duration rotation, revocation, archival verification, and dependency retirement would receive equal weight. Cross-party governance cost and usable recovery time would remain explicit outcomes.

That operational contract remains a prospective research target. Stronger support would require implemented constructions, independent verifiers, matched workloads, leakage and lifecycle testing, reproducible artifacts, and claim-specific review. Until then, the prose establishes neither cryptographic security nor authorization, semantic validity, end-to-end privacy, acceptable cost, or production readiness.

23.18 Codex test plan

Test	Purpose	Status
Guarantee-separation test	Seed cases where confidentiality holds but authorization, freshness, or semantic correctness fails; reject any aggregate `secure=true` result.	Lean evidence non-substitution and two impossibility results implemented; implementation campaign planned
Replay and mismatch test	Replay evidence and substitute model, tokenizer, policy, or preprocessing commitments; the verifier must fail closed.	Lean artifact, policy, epoch, and expiry invalidation implemented; real verifier planned
Leakage inventory test	Account for outputs, access patterns, timing, logs, caches, crash dumps, receipts, and verifier metadata.	planned; not run
Matched-cost test	Compare native and protected paths under equal task, quality, context, concurrency, and accounting boundaries.	planned; not run
Fallback observability test	Force protected-path failure and verify that no silent unprotected downgrade occurs.	Lean authorization and observability obligations implemented; executable failure injection planned
Independent appraisal test	Implement the verifier separately from the prover and test policy/version disagreement.	Lean role separation and policy invalidation implemented; independent implementation planned

23.18.1 Formalization hooks

lean:confidential-and-verifiable-ai-computation.admission_boundary is implemented by the 31 theorem declarations in AsiStackProofs.ProtectedComputationReview. The eight-step review preserves transaction and artifact identity, separated guarantee classes, evidence-role and statement scope, freshness, leakage, observable fallback, cross-owner handoff, and explicit non-authority. Its 48 admission-axis mutations all block readiness and receive exact repair or refusal dispositions before the only positive terminal state, a Project Theseus protected-computation campaign.

The formal surface includes evidence non-substitution: remote attestation does not establish semantic correctness, an encoded-relation proof does not establish authorization, and a confidentiality mechanism does not establish end-to-end privacy; finite leakage accounting is proved by induction over an arbitrary channel list. Artifact, verifier-policy, evidence-epoch, and expiry changes invalidate a bounded receipt; a leakage overrun remains rejected under more observation and no larger allowance; and unprotected fallback requires separate authorization plus consumer-visible disclosure.

The semantic-authority impossibility proves that identical attestation, relation-proof, and confidentiality signals can accompany opposite semantic and authorization states. The end-to-end privacy impossibility proves that identical input-confidentiality, model-confidentiality, and computation- integrity signals can accompany opposite output-and-metadata privacy states. A bounded bridge supplies threat and flow fields to AsiStackProofs.PrivacyInformationFlow while deliberately leaving purpose and authority false, so the privacy owner rejects rather than inherits them.

All dossier fields are authored assumptions. Lean does not prove cryptographic soundness, attestation validity, hardware trust, side-channel resistance, measured leakage, semantic correctness, authorization, privacy, fallback efficacy, acceptable cost, secure deployment, support, transfer, or external effect. Chapter support remains argument; support_state_effect=none. Project Theseus must run a competent protected-computation campaign with implemented constructions, independently written appraisers, replay and mismatch injection, side-channel inventory, matched native/protected workloads, observable fallback, recovery, and complete attempt denominators.

23.19 Source crosswalk

Source ID	Title	Planned use
`ext_nist_privacy_enhancing_cryptography_2026`	Privacy-Enhancing Cryptography	Planned use from inventory/manifest: NIST program material distinguishing fully homomorphic encryption, secure multiparty computation, zero-knowledge proofs, private-set intersection, and related privacy-enhancing techniques. It provides terminology and use-case context, not implementation security, usable performance, authorization, or end-to-end privacy.
`ext_zkllm_2024`	zkLLM: Zero Knowledge Proofs for Large Language Models	Planned use from inventory/manifest: Research prototype for proving bounded LLM inference claims while hiding model parameters. Reported proof size and latency are configuration-bound and do not establish semantic correctness, authorization, side-channel security, production readiness, or end-to-end privacy.
`ext_ietf_rats_architecture_2023`	Remote ATtestation procedureS (RATS) Architecture	Planned use from inventory/manifest: Primary IETF architecture and terminology comparator for Attester, Verifier, Relying Party, Evidence, Attestation Results, appraisal policies, reference values, freshness, layered environments, privacy, trust roots, and confidential-model key release. It is informational architecture, not a protocol, hardware assurance level, verifier-independence result, or local attestation deployment.

23.19.1 Publication placement and preserved technical ownership

In the consolidated publication argument, this chapter is the protected- execution dossier nested under Privacy, Data Rights, and Information-Flow Governance. It continues to own guarantee separation, distrust boundaries, attestation and proof statements, verifier policy, freshness, leakage, cost, fallback, and construction-specific limits. Privacy continues to own purpose, authority, affected parties, minimization, recipients, retention, rights, remedy, and the complete-enough information lifecycle.

The nesting is editorial, not evidentiary. Cryptographic validity cannot authorize a purpose or prove end-to-end privacy, and a privacy record cannot establish hardware trust, proof soundness, or side-channel resistance. This URL, its local claim, source mappings, proof target, test plan, and argument-level support ceiling remain independently reviewable.

23.20 Summary

Confidential computation, verifiable computation, remote attestation, privacy, and authorization overlap, but they are not interchangeable. The governing object is a compositional execution contract: named guarantees, adversary and leakage models, precise evidence statements, independent appraisal, freshness, matched cost, observable fallback, revocation, and explicit unsupported properties. This is an argument-level design. No protected-inference result has been reproduced here.

The main operational habit is to ask what exact statement a relying party may accept after checking a particular record. Every additional adjective needs a separate mechanism and residual boundary. If freshness, artifact identity, authorization, semantic translation, leakage accounting, or recovery is missing, the execution may still compute an answer, but it cannot inherit the stronger protected-computation claim. This separation makes failure diagnosable: a consumer can locate the problem in cryptography, platform state, artifact identity, semantic translation, authorization, or policy. It prevents a valid proof from laundering an invalid purpose and prevents a legitimate purpose from excusing unverifiable execution.

23.21 Handoff

Execution evidence ultimately depends on keys, artifact identity, measured platforms, and recovery authority. Continue to Model-Weight Custody and Hardware Roots of Trust. It receives exact guarantee, artifact, configuration, key, verifier, freshness, revocation, leakage, cost, and fallback fields. It does not inherit a claim that the protected computation is authorized, semantically correct, private end to end, or safe to release.