Instrument Repository

Problem

A global asset manager needed every downstream system to agree on what a financial instrument is, how it behaves under corporate actions, and which states are allowed. Implementations had drifted over time, creating subtle reconciliation failures—hard to detect in operations and hard to explain to regulators when two systems disagreed on the same instrument event.

Specification & verification

We expressed instrument behaviour as a compact Spec++ specification: a few pages of rules and 26 invariants describing legal states and allowed events. Those invariants were machine-checked, not only peer-reviewed. From that specification we generated production code.

What was shown

The specification decides which instrument states and corporate-action events are allowed. A corporate action is not free to cascade into the trading layer. Within that specification, Theorem 6.7 says corporate actions cannot cascade to the trading layer in unapproved ways. The sample is the pilot: 11 pages, 26 invariants, 8 formal proofs, generated into 3,829 lines with 36 tests.

What stays outside is anything the specification does not cover, and any system this pilot has not replaced.

How we delivered

We delivered it as a software engagement. Spec++ was the method for writing the specification.

Agentic Compliance Operator

Problem

A wealth manager wanted to let AI propose account rebalancing actions while guaranteeing that no proposal could ever breach mandate or suitability rules, even if the AI was compromised or adversarially prompted.

Specification & verification

We defined a security model in which the AI is explicitly untrusted. Every state transition in the workflow is guarded by formally specified policies and zero‑knowledge proofs. The validator enforces the rules; the AI never becomes the enforcement layer.

What was shown

The AI may propose a rebalancing action. The validator decides. The AI is not the enforcement layer. In the specified model, no adversary, including a fully compromised AI, can cause a non-compliant state transition. The sample is the wealth-management pilot: a PCAS security model, 4 theorems, and zero-knowledge circuits, on managed-account rebalancing.

What stays outside is whether those policies are the right reading of a mandate, and any claim that an examiner has accepted the record.

Supplier onboarding with proof-gated governance

Problem

Large institutions want AI agents to onboard suppliers faster—screening, document checks, status updates—without trading away compliance accountability. Most agent platforms log what happened; they do not prove that each status change was evaluated against a stated policy before execution.

Specification & verification

Policy is uplifted into a Spec++ specification—versioned, machine-readable rules compliance can sign off on. At runtime, CECO evaluates each agent-proposed transition before it runs: the agent is untrusted; the validator decides; ZK proofs can show three-way match rules satisfied without disclosing supplier pricing to the agent.

What was shown

The agent may propose a supplier status change. The Compliance Operator evaluates that transition against the pinned policy before it runs. The reference implementation can show, for a three-way match of purchase order, goods receipt, and invoice, that the rule held at decision time, without disclosing supplier pricing to the agent.

What stays outside is that this is a reference implementation, not a live onboarding book, and the record is not a claim that a regulator has accepted the check.

How we delivered

Delivered as a reference implementation of the Compliance Operator. Spec++ was the method for writing the policy.

OTC confirmation (look-alike screen)

Problem

This is one application of the Riley Betts Proof Fabric — portable trust, not a trading venue. OTC confirmation still sits on phone, email, chat, and each firm’s private logs. FIX carries the order. SWIFT carries the payment instruction. Neither carries a portable answer to: did both counterparties screen this trade, under stated rules, at a stated time — and agree the same terms?

Specification & verification

Two counterparty agents negotiate an OTC single-stock future. Each runs its own Compliance Operator gate against its own policy before execution. They co-sign one identical object — terms hash plus both compliance hashes — so there is no “my version vs yours.” A compact receipt (hashes, booked flag, timestamp) is then anchored on a chain neither firm owns. Ethereum stood in for Anchor. Validity stays in the off-chain certificate. The book never goes on-chain.

The hero scenario is not a fill. A buy-side restriction on an issuer also caught the look-alike future wrapper. The trade did not execute. Confirmation still recorded that both sides screened it, and that it was stopped.

What was shown

Each counterparty agent proposes. Each firm’s own Compliance Operator gate decides before execution. A look-alike future that fails the buy-side issuer restriction is not booked. The feasibility pilot records that both sides screened one OTC single-stock future under stated rules at a stated time, and that it was stopped. Ethereum stood in for Anchor.

What stays outside is that the chain attests existence and time, the certificate attests validity, the book stays off-chain, and this is not a venue and not Anchor in production. The case is an application of Proof Fabric.

How we delivered

Delivered as a feasibility pilot. Ethereum stood in for Anchor. The same pattern is reached through the Lean-proved software engagement.

OUCH FPGA bridge

Problem

A trading firm already checks an order before it can reach an exchange: size, price, how often orders are sent, and a way to stop new orders. Those checks usually sit in software on the same computers that send the orders. An agent, a person, or another program can still reach the session if another path, or another credential, exists.

Specification & verification

The research design places a Compliance Operator on an FPGA between the sender and the exchange. The preferred shape has two network ports. One faces the sender. One faces the protected session. Traffic is dropped unless the gate forwards it. The messages are Nasdaq OUCH, carried on SoupBinTCP. OUCH is short and binary, so a parser can reject anything outside a fixed size. SoupBinTCP is the session already described in the Lean ITCH work.

The policy this demonstrator is written to enforce covers six checks. Each order’s quantity, and quantity times price, stays inside a limit. The price stays inside a band, and the instrument is on an allowlist. Open orders and fills stay inside an exposure limit. The number of messages in a time window stays inside a rate. A kill switch blocks new orders and still allows cancels. A replace or a cancel refers to an order that is still live.

The claim to aim for is this. If a protected system executes an order through this gate, that order had a CECO authorisation for the current policy and for the state that policy depends on. In software, that check is a Lean proof. On the FPGA, the same policy is compiled into the circuit, through a HardCaml design and a checked link to the hardware description. The gate fails closed. If it cannot tell whether the exchange completed the order, the result is unknown.

A single-port action service is the other profile. It uses the same policy. It holds only when the protected session accepts orders from CECO alone.

What was shown

Components of the design have been tested in Verilator. Verilator is an open-source compiler that translates Verilog and SystemVerilog, the languages used to describe hardware, so those components can be run and checked before they are placed on a chip. Nothing has been shown on an FPGA yet. This case records the architecture and the property a demonstrator would have to show. The sender may be an agent, ordinary software, or a person. The gate decides before the order is forwarded.

What stays outside is the running appliance, which has no date. This is not a Nasdaq matching engine, not a certified exchange session, and not a finished OUCH product. Proofs of the software OUCH client do not cover the FPGA. Chip configuration, boot, keys, clock, the network ports, and the step from the proved model to the silicon sit outside the Lean proof. Two ports leave other paths open: a wireless link, a tunnel, a management interface, or a credential left on the sender’s host. Exposure, rate, and order-lifecycle checks need state from the exchange’s replies, and that state has to be trusted. Latency has not been measured. A regulator has not accepted the check.

How we delivered

This is research architecture. It is the hardware end of the same Compliance Operator, named on the product page as proved FPGA programming.