Development Fund Proposal Submission - DamlSec

OPENPull Request

by nevillegrech11-04-2026Incoming

Development Fund Proposal Submission

Proposal file: /proposals/damlsec-dedaub.md

---

Summary

DamlSec is a symbolic execution engine for DAML-LF that automatically detects security vulnerabilities — authorization gaps, conservation violations, arithmetic faults, rounding errors, privacy leaks - by analyzing compiled .dar files across all feasible execution paths. It uses a two-tier SMT strategy with a pure-Scala inner prover for fast path pruning and CVC5 for heavyweight property verification and counterexample generation. No existing tool provides automated, path-sensitive security analysis that operates directly on compiled DAML artifacts.

---

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

The tool reuses the Speedy Compiler pass and operates on compiled .dar artifacts, the same stable binary interface used by the rest of the Canton deployment pipeline. - The inner theorem prover is pure Scala with zero native dependencies, making distribution as simple as any JVM artifact on the DAML toolchain. - No existing tool fills this gap. - Very limited execution risk. - Dedaub has prior Canton/DAML audit experience and has built production-scale symbolic execution and static analysis tools for Ethereum used by over ten thousand registered users.