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.

Guarantee you can take to a regulator

We can say, with proof, that certain invalid states are architecturally impossible—not merely unlikely in testing. When a supervisor asks why a corporate action did or did not flow through to trading, we can point to a formally defined rule and evidence it was enforced—e.g. Theorem 6.7: corporate actions cannot cascade to the trading layer in unapproved ways within the specified model.

How we delivered

Delivered via software engineering with Spec++ SDD—the same engagement model we offer on your highest-risk reference data or instrument workflows.

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.

Guarantee you can take to a regulator

The system comes with named theorems: for example, that no adversary—including a fully compromised AI—can cause a non‑compliant state transition. Each decision is accompanied by a hash‑chained, cryptographically verifiable record that can be presented in an examination.

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.

Guarantee you can take to a regulator

For each onboarding decision you can produce a record showing what was decided, which rule applied, what state the system saw, any human approval, and cryptographic evidence the rule held at decision time—not a narrative rebuilt from CRM and ticket exports.