Proof-Carrying
Markets.

We made the action digital. We left permission in a document.

A machine can propose a thousand decisions before an institution can explain why one of them was allowed. This mismatch is becoming a design problem for markets.

A credit decision, a manufacturing release, an insurance settlement and an energy dispatch are not merely outputs. They change someone’s options, move resources or expose people to harm. Today, their justification is often distributed across contracts, databases, approval systems and the memories of specialists. The action travels faster than the reasons that authorise it.

Regulated industries already use preventive controls, validation and authorisation. The proposal here is not that all compliance happens after the fact. It is that the evidence remains fragmented: a reviewer has to reconstruct the relationship between the rule, the facts, the model, the authority and the specific action. When AI increases the number and speed of decisions, reconstruction becomes an increasingly fragile operating model.

Proof-Carrying Markets proposes a different unit of exchange: the action together with its inspectable permission envelope. An action would carry the exact claim it makes, the rule version applied, the evidence relied upon, its expiry conditions, the responsible authority and a verification result. Receiving systems could inspect that envelope before granting access to the mechanism that changes the world.

In the future, proof should travel with innovation. Permission would become a property of a specific action in a specific context.

This does not abolish licences, prior approvals or public authority. It makes applicable permissions computationally present at the point of execution. Regulation becomes part of the computational substrate: a dependency of the system’s behaviour, rather than an explanation assembled around it.

What, exactly, is being proved?

Proof-carrying code established a useful separation: a producer supplies code and evidence that it satisfies a consumer’s stated safety policy; the consumer checks that evidence before accepting the code. The pioneering work of Necula and Lee is the intellectual starting point, not evidence that entire organisations can already be verified. [1]

The organisational extension is a research thesis. Most real decisions will carry a heterogeneous assurance package, not a single mathematical proof. Its parts must remain visibly different:

That distinction prevents the most dangerous shortcut: labelling a signed model output “proof.” A language model’s fluent rationale is not a derivation. A successful policy evaluation is not a universal legal opinion. A signature on bad evidence makes the bad evidence attributable.

A decision should arrive with its own cross-examination.

The interesting artifact is not an approval badge. It is a structured answer to the questions an adversary would ask.

What action is authorised, for whom, in which jurisdiction, for what purpose and until when? Which version of the obligation was interpreted? Which observations were available then? Which model, prompt, retrieval corpus and tools participated? Which checks ran, which uncertainties remained, and who accepted the residual responsibility?

A production envelope would bind those answers to an action digest and an execution context. It would identify the evidence issuers, policy authors, evaluators and enforcement point separately. The agent proposing the action should not be able to silently change the rule that admits it. A small, independently governed verifier should check the package; a constrained executor should require the result.

The gap between checking and acting matters. An account can change, a safety notice can arrive, or a permit can expire after a check succeeds. Verification must therefore be bound to the exact action and relevant state, with short validity windows, replay protection and revalidation immediately before execution. Receipts also need to distinguish permitted, attempted and completed. An authorisation is not proof that an action happened.

There are useful building blocks today. NIST’s OSCAL provides machine-readable models for controls and assessment information; it does not automatically compile law into executable meaning. W3C PROV supplies a vocabulary for entities, activities and agents in provenance records. Open Policy Agent supports policy decisions and decision logging. These can support a runtime without constituting the proposed market architecture on their own. [2] [3] [4]

The law cannot be reduced to an if statement.

A legal text contains definitions, exceptions, proportionality, conflicts and open concepts. Turning it into software is an act of interpretation. That act requires provenance and accountable review as much as the decision it later controls.

The rule pipeline would begin with an authoritative source and an applicability analysis. Specialists would approve a formal subset, link every predicate back to its source and document what remains outside the model. Positive cases, counterexamples and boundary cases would test the interpretation. An LLM could propose mappings and locate contradictions; it should not publish binding policy from its own reading.

Cross-border execution makes this harder. A jurisdiction is not simply a dropdown: applicable obligations can depend on the actor, affected person, product, location, purpose and transfer path simultaneously. Requirements may overlap or conflict. The runtime must preserve those conflicts and route unresolved cases to a legitimate decision-maker, rather than choose whichever rule permits the action.

When a rule changes, the system should compute the affected dependency subgraph. Which pending actions relied on the old permission? Which model validations or reviewer attestations need renewal? Which completed actions require investigation? A historical receipt should retain the rule and evidence that were known at the time; it must not be silently rewritten to fit today’s policy.

In the simulation, a new rule changes the allowable evidence age. In practice, a change might alter an intended use, a population restriction or the meaning of adequate oversight. Some changes can propagate mechanically. Others invalidate the interpretation itself. The system must know the difference.

Bounded autonomy has somewhere to stand.

Ultra-regulated industries often possess assets that autonomous systems need: explicit responsibilities, documented procedures, validation practices, controlled access and defined escalation paths. Those arrangements are costly when every check requires a fresh human reconstruction. They could become an advantage when the reusable parts are converted into inspectable infrastructure.

In a bounded workflow, an agent would have a smaller admissible action space, a clearer evidence contract and a reliable way to abstain. Its freedom would expand only when the system can establish the necessary conditions. The same infrastructure could let supervisors see where autonomy stops, rather than discover the boundary after a failure.

The European Commission’s description of the AI Act’s high-risk framework includes logging, documentation, human oversight, accuracy, robustness and cybersecurity. That is evidence of an institutional demand for traceability and control—not an endorsement of this architecture, and not a claim that a proof receipt satisfies the Act. [5]

The paradox holds only conditionally. A well-defined policy can encode a harmful objective. A trusted issuer can report false facts. Several firms can share the same defective verifier and fail together. A system can obey every local rule while producing an unacceptable aggregate outcome. Safety requires empirical validation, adversarial challenge, operational monitoring and the ability to intervene outside the proof system.

The proposition is therefore precise: for appropriately bounded tasks, institutions with mature assurance practices may be better placed to deploy accountable autonomy than environments that equate fewer constraints with greater readiness. The evidence for that proposition must still be produced.

From a receipt to a new market primitive.

A proof-carrying decision is the smallest unit. A proof-carrying organisation would connect those units to mandates, delegation limits, process controls and the people accountable for them. It would be able to answer not only “Why did this happen?” but “Which assumptions made it possible, and which other decisions depend on them?”

A proof-carrying market would emerge when organisations can exchange and independently verify those objects. A supplier could attach evidence of a bounded release condition; a buyer could check it against its own policy; an insurer could inspect the relevant assurance claim; an auditor could reconstruct the sequence without accepting a slide deck as the system of record.

Interoperability would require more than a common JSON format. Parties need shared semantics, trusted issuer registries, revocation mechanisms, evidence access rights and ways to challenge a claim. A valid package in one institution may be insufficient in another. Composition requires checking the receiving context, not merely accumulating green ticks.

Cryptographic provenance can make alterations detectable and attestations attributable. Sigstore’s security model illustrates how identity, signatures and transparency infrastructure can support artifact verification. It also makes the trust assumptions visible. This is a useful engineering reference, not a requirement to put corporate decisions on a public blockchain. [6]

Privacy changes the design. Most recipients should receive the minimum evidence needed for a particular claim, not an institution’s entire internal record. Selective disclosure and, for suitable formal predicates, zero-knowledge proofs could reduce disclosure. They cannot guarantee the truth of the private inputs or resolve an ambiguous legal interpretation. Sensitive records need controlled access, retention limits and correction procedures; a public immutable log is not a default answer.

The commercial opportunity is a reduction in the cost of establishing warranted trust. The danger is a proprietary permission network that turns its owner into an unaccountable regulator. Open verification formats, independent implementations, portability and public contestability are constitutional requirements for this market idea.

Start with one decision that matters.

I would begin with a bounded manufacturing-release workflow: evidence is assembled for a batch, a model proposes a disposition, established checks evaluate a narrow policy, and the authorised human retains the release decision. No claim that a generic AI can certify a medicine; no expansion beyond the agreed validation boundary.

The first product would be an evidence graph, a policy registry, a verifier and a receipt interface integrated into the existing workflow. It would operate in shadow mode before controlling anything. The question is whether it catches missing authority, expired evidence and configuration drift while making disagreements easier to resolve.

Measure false permissions, unnecessary blocks, unresolved cases, evidence freshness, reconstruction time and the impact of policy changes. Report denominators and severity. Faster processing is useful only if it does not hide missed obligations or overwhelm reviewers. No universal target or performance claim belongs here before a real evaluation.

A business could sell integrations, validated workflow modules and operational assurance. Its durable advantage would be reliable evidence and trusted interpretation, not an enormous language model pretending to be a regulator. Verification should remain independently possible even when the vendor disappears.

Who is allowed to define “permissible”?

If a society encodes permission, the authors of the encoding acquire power.

The hardest work is governance: who may create a rule, challenge an interpretation, revoke a credential, inspect the evidence or authorise an exception? Affected people need intelligible reasons and meaningful appeal. A machine-readable denial that nobody can contest is an automated bureaucracy with better logging.

The runtime must represent uncertainty without laundering it into certainty. A non-executable result can mean a prohibition, missing evidence, an unavailable dependency or unresolved interpretation. Those are different situations with different remedies. The interface may need a binary execution gate; the explanation must preserve the richer state beneath it.

Failing closed also has consequences. A blocked action can delay treatment, interrupt supply or remove access to an essential service. Operational design needs bounded escalation, human continuity procedures and explicitly governed emergency powers. An emergency exception should create a new attributable record with its own scope; it should never erase the failure that required it.

Proof-Carrying Markets would succeed if it made responsibility more legible and contestable as machines become more capable. It would fail if it replaced institutional judgment with the appearance of mathematical inevitability.

The future of regulated innovation is not permission without responsibility. It is responsibility that can travel at the speed of the action.