# What a Proof Is Allowed to Mean A guide to the missing receipt around proof artifacts: how proof bytes, statement meaning, verifier domain, and replay assumptions become one accepted object. Authors: [Omar U. Espejel](/about/) Published: 2026-05-07 Updated: 2026-05-26 Tags: tablero, verifiable ai, zkml, proof systems ## TL;DR - A proof verifier answers a narrow question: did these bytes satisfy this relation? - A zkML application needs a wider receipt: this model, this input, this output, this verifier domain, and this policy. - If those facts are loose labels beside a proof, the proof can verify while the public claim is still wrong. - In this series, I call the typed boundary that binds those facts a Tablero. - Tablero is not a new proof system. It is the receipt that makes proof artifacts harder to relabel and easier to compose. Series part 4 of 4 The first three essays explain the shape, the pressure, and the statement problem. Part 4 explains the receipt a proof artifact needs before an application should trust what it means. This is not about inventing a new proof protocol. It is about the boundary around a proof: what a verifier accepts, what that object means, and what downstream layers are allowed to skip. [Part 1](/essays/why-transformers-fit-starks/) said transformer decode is trace-shaped. [Part 2](/essays/where-transformer-proof-pressure-appears/) said proof pressure concentrates around lookup-heavy attention work, range policy, rounding, and carried state. [Part 3](/essays/proof-validity-is-not-statement-validity/) said proof validity is not statement validity. Now imagine someone hands you a proof and says: > verified. That is not enough. Verified against which model? On which prompt? With which output commitment? Under which numeric policy? Using which verifier? Inside which deployment event? If those answers live as loose labels beside the proof, the proof can still verify while the product claim is wrong. The model label can drift. The prompt can be swapped. The verifier domain can change. The policy can be renamed. The same bytes can be used as a receipt for the wrong thing. So a proof should not travel alone. It should travel with the statement it is allowed to mean. It should also say which dependency the next layer is allowed to stop replaying. In this series, I call that typed boundary a **Tablero**. The name is not the important part. The discipline is. ## Why this object has to exist A proof verifier usually answers a narrow question: > did these proof bytes satisfy this relation? A product wants to answer a wider question: > can I trust this receipt for this model event? The second question contains facts the proof verifier may not see by default: - which model; - which input; - which output; - which numeric policy; - which lookup table; - which verifier domain; - which proof artifact; - which deployment or action context. If those facts are loose labels next to the proof, they can drift. The proof can still verify. The claim can still be wrong. That is why Part 3 mattered. The typed boundary is the object that refuses to let the proof and the claim drift apart. ## The boundary object A Tablero is a typed verifier boundary. In plain language: > it is the object a downstream verifier is allowed to accept instead of reconstructing every fact behind it. The object binds five things. First, the proof artifact. Not "some proof exists." The specific proof, or a digest of the proof, has to be part of the accepted object. Second, the statement. For zkML, this usually means model identity, input commitment, output commitment, relation kind, policy label, and version or domain label. Third, typed handles. The object should distinguish a model commitment from an input commitment, a lookup-table handle from a tensor handle, and a proof digest from a carried-state root. Fourth, the verifier domain. The same bytes should not silently move between verifier contexts. Fifth, the replay manifest. This is the part people often skip. The boundary should say: > this downstream verifier no longer needs to replay dependency X, because the boundary is already bound to it. That dependency is not ignored. It is named. It is committed. It is part of what the boundary means. The short version: > proof + statement + typed handles + verifier domain + replay manifest. All accepted together. Not loose metadata. Not a README beside a proof file. The accepted object. ## Why typed handles matter Suppose a boundary carries a handle called `abc123`. What is it? A model commitment? A tensor commitment? A lookup table? A policy? A proof digest? A carried state root? If the system cannot tell, composition becomes fragile. Typed handles force the artifact to say: - this is the model commitment; - this is the input commitment; - this is the output commitment; - this is the carried-state handle; - this is the lookup-table handle; - this is the proof digest; - this is the verifier domain. That is not ceremony. It is how the object keeps meaning when it moves between layers. ## Why the replay manifest matters Most proof discussions stop at: > the proof verifies. Tablero asks another question: > what did this boundary let the next verifier stop replaying? That matters in layered systems. One layer verifies a proof. The next layer verifies the proof and reconstructs an old manifest. The next layer verifies the proof, reconstructs the manifest, rehashes old JSON, checks old source handles, and confirms that a previous chain still points to the next one. At some point, the verifier is not paying for new cryptography. It is paying to replay old bookkeeping. A Tablero boundary says: > this bookkeeping dependency was dropped here, and the drop itself is bound to the accepted object. That is the difference between skipping work and pretending work never existed. Tablero does the former. It should never do the latter. ## How this connects to the proof-pressure result Part 2 studied proof boundaries. It asked whether attention arithmetic and lookup-heavy table membership should live in one native proof object or in separate objects. That is an efficiency question. Tablero asks a neighboring correctness question: > once the proof object exists, what statement is it allowed to carry? If the proof surface is fused, the fused artifact still needs a typed statement boundary. If the proof surface is split, the pieces need typed boundaries so the next layer can compose them without losing the claim. So the two ideas are complementary: - proof-pressure boundaries choose efficient proof structure; - Tablero boundaries preserve application meaning. That is the architecture story. ## What Tablero does not prove Tablero does not prove that a model answer is true. A proof of execution is not a proof of factual correctness. Tablero does not make transformer proving cheap by itself. The inner prover still has to do the work. Tablero does not give recursion for free. If you want one proof for many proof objects, you still need a real recursive or accumulating backend. Tablero does not fix an underconstrained inner relation. If the proof system accepts the wrong computation, the boundary cannot make that computation right. The clean non-claim is: > Tablero does not make transformer proving cheap. It makes accepted proof artifacts harder to mislabel, easier to compose, and safer for downstream software to consume. ## The takeaway A proof is not self-explanatory. A statement envelope fixes part of that. Tablero goes one step further: > bind the proof, bind the statement, type the handles, name the verifier domain, and record what the next layer is allowed to skip. That is the object downstream systems should consume. Not loose proof bytes. Not product labels floating beside a verifier call. Not replay work disguised as verification. A typed boundary. That is the bridge from transformer proof structure to verifiable AI systems that can actually compose.