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
- [x] Proposal file added under
/proposals/ - [x] Milestones and funding amounts defined
- [x] Acceptance criteria included
- [x] 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.
