Proving Prova's receipts cannot be forged
A tamper-evident receipt is only as good as the math under it. Here is what we have proven about Prova's signing, policy engine, and multi-agent composition, and what we have not.
A receipt that says "this AI decision happened, and here is the signed proof" is only worth something if three things hold: the signing is sound, the policy that judged the decision is internally consistent, and the guarantee survives contact with an adversary. Claiming that is easy. We wanted to check it.
So we built three offline verification harnesses against Prova's real code. They are dev-only tools, not part of the product runtime, and they exist to hold our own claims to account. Here is what they establish.
The receipt is unforgeable, reduced to a standard assumption. Forging a Prova receipt without the private key reduces to either breaking Ed25519 (the signature scheme) or finding two different payloads that canonicalize to the same bytes. We wrote out that reduction, added a property test that the canonical form is injective (distinct payloads produce distinct bytes), and an adversarial suite that tries to forge, replay, and tamper with receipts. Everything an attacker can do without the key fails the verification step.
The canonicalizer is identical in every language. A receipt is signed over a canonical JSON form. If the server and an auditor's verifier disagree on those bytes by even one character, verification breaks. Writing the proof surfaced a real divergence: the Python verifier was rejecting genuine receipts that contained small floating-point numbers, because Python and JavaScript print them differently. We fixed the Python canonicalizer to match the server byte for byte, fuzzed it against tens of thousands of values, and now a receipt verifies identically whether you use our SDK or plain OpenSSL.
The policy set has no hidden contradictions. We translated Prova's policy rules into an SMT solver and checked two properties: that no permissive rule is silently overridden by a stricter one on the same event, and which kinds of events no policy governs at all. The built-in set came back consistent, and the coverage gaps it reported were the expected ones.
Multi-agent composition has a measurable safety obstruction. When several agents share resources, "each one is safe alone" does not imply "they are safe together." We model the part of that problem that is cleanly measurable, separation-of-duties conflicts and ordering races, and compute whether a safe global assignment exists at all.
A note on honesty, because it matters more than the claims. These are offline harnesses, not a feature you switch on. They depend on solver and cryptography libraries that are not Prova dependencies. The deepest piece, a machine-checked Lean proof behind the composition result, lives in a separate mathematics repository that is not part of the Prova codebase, so that specific claim is not independently verifiable from our open code today. We would rather tell you exactly where the proof lives than imply more than we can show.
The receipt is the moat. This is us checking that the moat holds.