Thank you for the thoughtful review and constructive feedback. We appreciate the recognition of the proposal's technical rigor and are glad the value proposition resonates. Below we address the two areas flagged for clarification.
1. Evidence of Ecosystem Demand
The demand for formal verification of CIP-0056 and CIP-0047 is both structural — arising from the role these standards play in the ecosystem — and externally validated by regulatory developments and direct engagement with financial institutions.
1.1 Regulatory momentum: the ACPR-AMF Smart Contract Certification Report
Report: https://www.amf-france.org/en/news-publications/news/acpr-and-amf-publish-findings-working-group-smart-contract-certification-and-launch-public
In February 2025, the French financial regulators ACPR and AMF published the report of their joint Fintech Forum Working Group on Smart Contract Certification. This report — in which TKNFRA's CEO (Zakaryae Boudi) participated as a working group member — explicitly identifies formal verification as providing "the highest possible level of assurance" for smart contract correctness (Section 1.2.3) and recommends it as part of a future EU-level mandatory certification framework for financial smart contracts.
Key findings from the report that directly support this proposal:
- Formal verification is singled out as the method that "aims at demonstrating compliance with the specifications in a logical-mathematical sense" and provides assurance that "can never be absolute" but is higher than any other analytical method (p. 29-30).
- The working group concluded that mandatory certification with proportionality measures — including formal verification for the most critical standards — is the regulatory option that "could provide the most guarantees for users and investors, without unduly hampering innovation" (p. 3, 48).
- The report explicitly states that code transparency alone is insufficient: "code transparency does not have the same impact as a certification mechanism" (p. 8). Machine-checked verification is positioned as a necessary complement.
- The report notes that formal verification methods are "ideal for assessing whether the smart contract code satisfies the compliance principles" — i.e., checking that a program actually performs the expected operations (p. 31).
- The ACPR-AMF framework envisions certification tied to specific code versions with re-certification upon changes (Proposals 13-14) — precisely matching our proposal's approach of pinning verification to Splice package versions/DAR hashes and providing a regression playbook.
This regulatory trajectory means Canton's core financial standards (token transfers, settlement, reward attribution) will face formal verification expectations from European regulators. Our proposal positions the Canton ecosystem to meet this demand proactively rather than reactively.
1.2 Direct engagement with financial institutions
Through our participation in various working groups and manifestations alongside major financial institutions, we have had direct discussions that confirm institutional demand for formal verification artifacts. The consistent feedback from these institutions is that:
- Banks and custodians evaluating Canton-based infrastructure ask for machine-checked evidence of correctness before committing to integration — standard security audits and test suites are necessary but not sufficient for financial-grade assurance.
- Auditors are actively developing frameworks for smart contract certification that rely on formal verification outputs as primary evidence. Our verification reports and proof artifacts are designed to slot directly into these emerging audit workflows.
- Compliance teams at regulated institutions need to demonstrate to supervisors that the financial primitives they depend on have been verified against stated invariants (conservation of value, atomic settlement, no double-spend). The invariant catalog and traceability matrix we propose are the artifacts these teams are looking for.
1.3 Structural ecosystem demand
CIP-0056 is foundational infrastructure. Every wallet, application, and token registry building on Canton depends on the correctness of the token standard's semantics — transfer instructions, allocations, and settlement. As the number of independent integrators grows, so does the cost of ambiguity or undetected inconsistencies in the standard. Formal verification provides a shared, machine-checked reference that all participants can rely on, reducing integration risk and support burden.
Canton targets regulated financial use cases. As Canton matures toward production financial deployments, institutional participants (banks, exchanges, custodians) will require machine-checked assurance artifacts. The ACPR-AMF report confirms this is not a hypothetical future — it is an active regulatory workstream with a proposed EU-wide framework.
Precedent from analogous ecosystems. Ethereum and Tezos have invested significantly in formal verification of core standards and smart contract primitives (e.g., ERC-20 verification efforts, Tezos's Michelson formal semantics). Given Canton's explicit enterprise and financial positioning, it should meet or exceed this bar. Providing machine-checked specifications signals maturity and seriousness to prospective ecosystem participants evaluating Canton against alternatives.
Upgrade safety for maintainers. Without formally stated invariants, changes to CIP-0056 or CIP-0047 can silently break assumptions that downstream integrators depend on. Maintainers of the Splice reference implementation currently lack a systematic way to verify that upgrades preserve the standard's semantic guarantees. The formal model and regression playbook directly address this gap — they are tools for maintainers, not just about the standard.
Auditor and compliance expectations. Third-party auditors reviewing Canton-based deployments will increasingly look for formal evidence of correctness in the financial primitives layer. The ACPR-AMF report makes clear this is the direction of travel for EU financial regulation. Providing verification reports and proof artifacts proactively positions the ecosystem to meet these expectations rather than retrofitting assurance after the fact.
2. Adoption and Usability
We designed the deliverables with distinct user groups in mind, and we recognize that the proposal should make this mapping explicit. Here is how each artifact serves its intended audience:
Deliverable-to-Audience Mapping
| Deliverable | Primary Audience | How They Use It |
|---|
| Plain-English invariant catalog | Developers, integrators, auditors | Understand what guarantees the standard provides without reading formal notation |
| Traceability matrix (CIP clause ↔ B model ↔ Daml element) | Developers, integrators | Find the formal counterpart of any CIP requirement; confirm coverage |
| Conformance contract | Third-party registry implementers | Minimal spec of assumptions and observable behaviors needed to comply with the standard |
| Verification reports | Auditors, compliance teams, governance | Review scope, proven properties, known gaps, and reproduction steps |
| Proof / model-check artifacts (CI-runnable) | Maintainers (Splice team) | Run pass/fail checks on every PR — no B-Method expertise required |
| Reviewer guide ("How to use the model in PR review") | Maintainers, contributors | Step-by-step guidance for using the model during code review, written for developers |
| Regression playbook | Maintainers | When CIP text or Splice interfaces change: what to update, how to re-verify, how to interpret diffs |
Accessibility by Design
- Dual-format invariant catalog. Every invariant is stated in both plain English a
