Proposal: B-Method Formal Verification Models for Canton DAML Standards (CIP-0056, CIP-0047)
Needs ChampionPR- SIG
- daml-tooling
- Champion
- —
- Author org
- —
- Ask
- 410,000
Abstract
TKNFRA proposes to deliver a B-Method-based formal verification model (spec + invariants + machine-checked evidence) for the Canton DAML standards CIP-0056 (Token Standard) and CIP-0047 (Featured App Activity Markers), tied to specific released Splice reference packages. This provides reusable assurance artifacts for wallets, apps, registries, and maintainers, and a regression playbook for upgrades.
Milestones
| Title | Due date | Target | Amount (CC) |
|---|---|---|---|
| Scoping + Formal Invariant Catalog + Model Skeleton (CIP‑0056 & CIP‑0047) | — | — | 75,000 |
| CIP‑0056: Core Workflow Formalization + Machine-Checked Evidence | — | — | 130,000 |
| CIP‑0047: Full Marker Model + Proof/Check + Accounting Consistency | — | — | 130,000 |
| Reference-Implementation Alignment + Upgrade/Regression Playbook | — | — | 75,000 |
| Total | 410,000 | ||
Budget impact
- % of approved-to-date
- 0.5%
- % if all RFV pass
- —
RFV scenario unavailable — using approved-to-date as denominator (degraded mode).
- Ask (CC)
- 410,000
Comments by org
2 comments · 1 org · last activity Mar 26, 2026
| Organisation | Comments |
|---|---|
| Canton Foundation | 1 |
| Unknown | 1 |