Proposal: Verified DAML applications with Quint - Specification-Driven Testing and AI-Assisted Smart Contract Development for Canton
Development Fund Proposal Submission
Proposal file: /proposals/informal-systems-verified-daml-applications-with-quint.md
Summary
This proposal aims to bring formal specification and model-based testing to DAML applications on Canton. It delivers:
- A spec-driven LLM code generation workflow where a Quint specification of the intended behavior guides an LLM to produce DAML code.
- Quint connect for DAML, a framework that automatically verifies a DAML contract against its Quint spec by replaying generated traces.
For the Canton ecosystem this raises the baseline correctness of DAML applications, introduces a practical specification-first discipline accessible to application developers, and makes AI-assisted DAML development verifiable.
Checklist
- Proposal file added under
/proposals/ - Milestones and funding amounts defined
- Acceptance criteria included
- Alignment with Canton priorities described
Notes for Reviewers
Informal Systems is a research and engineering company specializing in formal methods, distributed systems, and blockchain infrastructure. Among other achievements, we were the originators and lead developers of Malachite, a high-performance BFT consensus engine, until it was acquired by Circle in August 2025.
Quint is Informal's open-source executable specification language in the It includes a built-in simulator, model checker, and support for the ITF trace format used by quint-connect (a library for model-based testing of Rust applications). It is actively maintained and has been adopted for specifying distributed protocols, consensus algorithms, and smart contract systems.