Cryptographic objects, theorems, mechanization roadmap.
We are the only RWA stack inviting public mechanization of its security claims. Send us your counterexample.
Seven results across the Crypto Spec and Flow paper.
Every theorem below is stated formally in the cited section. Proofs are in the appendices. Mechanization in EasyCrypt and Tamarin is on the public roadmap.
PG[Σ] unforgeability
No probabilistic polynomial-time adversary can produce a valid PG[Σ] signature on a transcript whose PolicyHash differs from the active ComplianceModule, except with negligible probability.
Crypto Spec §6, Theorem 1
PolicyHash binding
The Fiat–Shamir transform binds the PolicyHash into the signature transcript such that any tampering with the policy invalidates verification.
Crypto Spec §6, Lemma 6.4
CGM strategy-proofness
Under continuous trading, no strategic agent can improve their utility by misreporting their type or their order parameters in the compliance-gated matching mechanism.
Crypto Spec §9, Theorem 2
Route admissibility soundness
A verifying party accepts a route certificate if and only if the predicate J ∧ T ∧ ID ∧ X held along every hop of the route at certificate-construction time.
Flow §7, Theorem 3
Cross-chain certificate unforgeability
No adversary controlling fewer than t of n committee members can produce a valid cross-chain certificate, even under arbitrary network adversary.
Crypto Spec §10, Theorem 4
DvP atomicity
The delivery-versus-payment protocol terminates either with both legs settled or with both legs aborted, even under partial network failure of up to (n − t) committee members.
Crypto Spec §11, Theorem 5
Liquidity pool composability
Two L3RS-1 assets that share a compatible ComplianceModule can be routed by Flow under a single composed admissibility predicate, without re-issuance and without weakening either policy.
Flow §16, Theorem 6
EasyCrypt and Tamarin. Public dates.
We commit to mechanizing the two highest-stakes theorems with two different proof tools, on a public schedule. Both projects are open-source.
EasyCrypt
Target Q4 2026PG[Σ] unforgeability proof under mechanized game-based reductions. EasyCrypt was chosen because the PG[Σ] proof is a sequence of game-based reductions over a Fiat–Shamir transform, which EasyCrypt was designed for.
Status: code-and-comment phase, lead by [TBD]
Tamarin
Target Q1 2027Cross-chain certificate protocol model with secrecy and authentication lemmas under arbitrary network adversary. Tamarin was chosen because the cross-chain protocol is a multi-party protocol with timing constraints and a heterogeneous committee.
Status: protocol model in draft, lead by [TBD]
A public harness, in progress.
A public reproducibility harness covering the Flow ablation studies, the PG[Σ] verification harness, the CGM strategy-proofness simulator, and the cross-chain certificate test vectors lands in Q3 2026. Every benchmark we publish on this site or in the papers will be reproducible from the harness with one command.
If we cannot reproduce a number on the public harness, we will not publish it. That is the eighth item in the “What we will not say” list, and it is not a slogan — it is a constraint we built the documentation around.
Subscribe for the launch announcement at research@t3rra.co.
What we have not yet proved.
A live list lives in Crypto Spec §15 and Flow §17. Highlights:
- A tighter bound on the adaptive adversary against PG[Σ] under non-uniform polynomial-time reductions.
- Strategy-proofness of CGM under partial information and bounded-rational agents.
- A formal model of the AI re-ranker inside the PG[Σ] envelope, with a stated non-interference theorem between the model output and the signature.
- A fully mechanized proof of the (5,9) committee under arbitrary network adversaries with timing constraints.
- A liveness bound on cross-chain certificate construction under intermittent committee availability.
- A composability theorem for L3RS-1 ComplianceModules across non-compatible jurisdictions, under a meet-semilattice of policies.
- A formal definition of "compliance equivalence" between two PolicyHashes that name the same legal effect in different jurisdictional vocabularies.
- A privacy-preserving variant of the route admissibility predicate using zero-knowledge proofs.
Selected references.
The full bibliography lives in each paper. The selection below is what we cite the most often in academic correspondence.
(More references in each paper's bibliography.)
Send us your counterexample.
We mean it. The fastest way to make this stack better is to break it on paper before we ship it on chain.
Email research@t3rra.co