#12Needs Champion Pull Request
Proposal: B-Method Formal Verification Models for Canton DAML Standards (CIP-0056, CIP-0047)
zakaryaeboudittv21-02-2026Last activity 6mo ago
daml-tooling
Development Fund Proposal Submission
Proposal file: /proposals/tknfra-bmethod-formal-model-daml-standards.md
Summary
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.
Checklist
- Proposal file added under
/proposals/ - Milestones and funding amounts defined
- Acceptance criteria included
- Alignment with Canton priorities described
Notes for Reviewers
- Scope is intentionally limited to standards (CIP-0056, CIP-0047) and their reference packages; not a general-purpose Daml verification toolchain.
- We welcome guidance on preferred repository location for deliverables (Canton Foundation org vs. TKNFRA org) and any preferred proof/model-check tooling constraints for CI.