Why post-trade tokenisation needs a shared, machine-readable catalogue of correctness properties: the load-bearing beam beneath the rulebooks already written.
Tokenfrastructure Team//11 min read
A catalogue of the promises a tokenised system must keep, and what it would take to prove them
For an industry that has spent the better part of three years insisting that tokenisation will remake the plumbing of global finance, the post-trade establishment has been conspicuously busy agreeing with itself.
In the space of two years, the world's largest financial market infrastructures have produced a control framework for digital-asset securities, an interoperability framework to follow it, and a steady drumbeat of pilots moving real instruments onto distributed ledgers. DTCC, Clearstream and Euroclear, institutions that between them sit beneath a very large share of the world's settled securities, have written down, in unusual concord, what a tokenised market ought to look like. The industry has, in parallel, settled on ISO 20022 as the common grammar for the data those markets exchange.
What it has not done, according to a small open-source project that has begun to attract attention in the narrow world where formal methods meet financial infrastructure, is build the part that matters most once the rulebooks are written and the code is deployed: a way to prove, rather than merely assert, that a given system actually does what the frameworks demand.
The project is called the Blockchain Property Ontology. It is public, it is unfinished, and its central claim is uncomfortable: that the tokenisation effort, for all its standards-setting, has been assembling the scaffolding of trust without the load-bearing beam.
The gap nobody owns
The argument rests on a distinction that sounds pedantic and turns out to be expensive.
A control framework, the Digital Asset Securities Control Principles, or DASCP, published by the three infrastructure giants, is a rulebook. It says, in effect, that a tokenised-securities system should have an emergency-stop mechanism, fine-grained controls over who may do what, a guarantee that settlement once final cannot be undone, and several dozen other things besides. These are the right requirements. They are also, by their nature, prose: a document a human reads and a committee approves.
A rulebook, however, cannot be executed. It cannot be checked by a machine. And it cannot tell an institution how to establish that the smart contract it is about to entrust with several hundred billion euros of commercial paper genuinely enforces the control the rulebook names, not in the cases someone thought to test, but on every path the code can take.
That is the gap. On one side, a control the industry agrees it needs. On the other, a smart contract that may or may not enforce it. Between them, today, sits an audit: a human exercise, re-derived from scratch each time, encoded in no shared language, and offering assurance that decays the moment the code changes. "The most popular assurance tools in this market examine one execution at a time," the project's documentation notes, in a passage that doubles as an indictment.
Point such a tool at a property it cannot in principle establish, whether a system leaks private data, say, collect a clean report, and you have not been given weak evidence. You have been given a category error dressed up as assurance.
The Blockchain Property Ontology is an attempt to fill that gap with something the industry has, oddly, never built: a shared, open, machine-readable catalogue of the properties a tokenised system is supposed to have, and, for each, a precise account of what it means, how it can fail, what it depends on, and how it could actually be proven.
A periodic table for correctness
Strip away the terminology and the idea is close to the periodic table. Before it, chemistry was a heap of disconnected facts; the table gave every element a stable identity and a position relative to every other, so that everyone's experiments could add up. The ontology proposes to do the same for the promises a financial system makes about its own behaviour.
Each entry is a single such promise, written three ways at once. There is a plain-language statement a non-specialist can read. There is a formal, mathematical statement a specialist cannot misread. And there is a structured, machine-readable version that a verification tool, or an artificial-intelligence auditor, can consume directly. "No units of an asset can be created except by an authorised party, on every reachable path." "A holder can always recover their own assets." "A settlement, once final, can never be reversed." Each is given a permanent, deliberately meaningless identifier, so that a reference to it survives even as the entry is rewritten, the same discipline that lets a citation to a known software weakness mean the same thing a decade later.
The catalogue is, by its authors' own admission, an early seed: a couple of dozen fully-worked properties, chosen to stress every part of the design rather than to cover the field. What makes it more than an academic exercise is the second thing it has done: connected itself, carefully and publicly, to the very frameworks the industry has just finished agreeing on.
Three bridges, and a chain
The catalogue's distinctive move is to bridge itself to three artefacts the industry has already published and broadly endorsed. Each bridge is mechanically checked; none claims more than it can support.
1. The control framework
The first connection is to DASCP. The catalogue maps the behavioural controls in the framework, access control, settlement finality, the emergency-stop family, and others, to the precise properties that capture them and to the methods that could establish each. The mapping is conservative to the point of severity: it claims to fully prove none of the controls, marking every link merely "supports" or "partially supports," on the grounds that each control bundles behavioural substance with operational and legal obligations that no single property can discharge. Every link is checked by machine, so the bridge cannot quietly rot as either side evolves.
2. The data standard
The second connection is to ISO 20022, and it is the technically novel one. The catalogue binds its properties to the data standard not only at the level of whole messages but down to the individual mathematical symbols inside each property: the identifier in a settlement-finality property tied to the standard's own SettlementTransactionIdentification, its status to the standard's TransactionStatus. A validator confirms, for every such binding, both that the data element exists and that the symbol genuinely appears in the formal statement: a check designed to make the fashionable claim of being "ISO 20022-native" something a machine can verify rather than a phrase in a pitch deck.
3. The interoperability framework
The third connection, added most recently, is to the interoperability framework the same three infrastructures published this year. Here the project's restraint is most telling. Of the framework's twenty-nine "building blocks," the catalogue cross-walks just nine, the ones describing what a ledger actually does, and explicitly records the other twenty as out of scope: legal recognition, identifier schemas, role taxonomies, licensing regimes, service-level targets. These, the project insists, are "agreements among institutions," not behaviours a system can be proven to satisfy, and sweeping them in to inflate coverage "would be the category error this catalogue exists to prevent." A lesser effort would have strained to map all twenty-nine and called it comprehensive. This one maps nine, says so plainly, and explains why the rest are someone else's layer.
Joined together, the three bridges produce a single chain that runs, in the project's telling, from a business instruction in ISO 20022, through an abstract operation such as "settle," to the formal property that governs it, and back to the standard's own data: a continuous path from what the business asked for to what must provably be true. The chain closes, end to end, in the live catalogue today, and a continuous-integration gate confirms every link in it resolves. It is, in the project's phrase, the connective tissue between what the rulebook requires and what the code provably does.
The discipline of saying less
The most striking feature of the work, for a field accustomed to vendors promising that their tool has found all the bugs, is how strenuously it refuses to overclaim.
It distinguishes, as a first-class matter, the promises that can be checked one case at a time from those that fundamentally cannot, privacy, the soundness of certain cryptographic proofs, fairness in ordering, and tags each property accordingly, so that no method may claim more than it can deliver. It records, for every guarantee, the assumptions it rests on, and treats an assumption nobody has yet discharged not as an embarrassment to be hidden but as a known, written-down risk: a guarantee of settlement finality, the catalogue notes, bottoms out at the assumption that the underlying ledger will not suffer a deep reorganisation, and it says so rather than pretending the problem away. Where two desirable properties genuinely conflict, an always-available exit against an emergency pause, it records the tension instead of smoothing it over.
This is, in a sense, an unusual thing to market. But for the institutions the project is courting, the austerity is the point. An infrastructure whose entire value is being trusted has seen enough green-checkmark assurance theatre to distrust a catalogue that claims to have solved everything; one that states precisely what it does and does not cover, and lets a machine enforce the boundary, is the one worth taking seriously.
"Here is exactly what we guarantee," the documentation says, "and a validator proves we are not overstating it." It is not a limitation. It is, the authors argue, the qualification.
Why now
The timing is not accidental. Two forces are converging on exactly this gap.
The first is that tokenisation is leaving the laboratory. Programmes once described as experiments are being readied for production settlement, in some cases against central-bank money. At that point "the code seems fine" stops being an answer a board or a supervisor will accept, and the difference between a control that is tested and one that is demonstrably enforced becomes the difference between a deployment that satisfies a regulator and one that merely runs.
The second is artificial intelligence. As automated and AI-assisted tools begin to write, audit and even operate parts of this infrastructure, the danger is plain: a machine proves what it is asked to prove, not what was meant. The project's framing of its own role in that future is precise: an AI is only as trustworthy as the specification it is checked against, and a precise, shared, honest specification of what these systems must guarantee is exactly what turns automation from a hazard into a tool. The catalogue, in this reading, is not a rival to the AI auditors coming down the track. It is the thing that makes them safe to use.
There is, too, an invitation the project did not have to manufacture. When the three infrastructures published their interoperability framework, they closed it by calling for industry working groups, under the sponsorship of the market infrastructures themselves, on, among other things, "smart contract integrity and change management" and a "smart contract model." It is difficult to read those words and the description of the Blockchain Property Ontology side by side without concluding that the FMIs have described, in their own document, the thing this project has begun to build.
An open question
Whether it succeeds is, candidly, an open question, and it turns less on the technology than on adoption. A shared map of correctness is worth precisely as much as the number of people reading from the same one; an open catalogue with a couple of dozen entries, however rigorous, is not yet a standard. The work needs the institutions that live these problems, the depositories, the infrastructures, the supervisors, to populate it, cite it, and shape it, the way ISO 20022 and DASCP themselves became load-bearing only once the industry agreed to lean on them.
But the proposition is a serious one, and it arrives at a moment when the industry's own published direction seems to be pointing at it.
The rulebook, the grammar and the proof
The technologies the world ends up trusting with the most, aviation, medicine, cryptography, earned that trust not through any single clever mechanism but through the slow accumulation of shared, rigorous, openly-built knowledge about what correctness means and how to establish it.
Post-trade is now building its own version of that body of knowledge.
It has the rulebook and it has the grammar.
What it has lacked is the proof.
The Blockchain Property Ontology is public at github.com/TKNFRA/blockchain-property-ontology, where its cross-walks to the DASCP and interoperability frameworks and its ISO 20022 binding can be inspected and verified.
