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

• [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

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.