RFP 22: a machine-checked semantics of Daml-LF 2, seeking a Tech & Ops champion

Hi all, I’m Frank Gruber at Obsidian Systems.

Every Daml analysis tool works from its own model of how Daml behaves. No public, machine-checked semantics of Daml-LF 2 exists to test those models against. A tool with a wrong model can report an unsafe package as safe.

We’re preparing a Dev Fund proposal under RFP 22 (Daml Security Standards and Secure Development) to build an executable semantics of Daml-LF 2.x and the Canton ledger model in Agda, in a public Apache-2.0 repository. Over 12 months it delivers:

• A core semantics that agrees with the Daml engine on the Daml Script tests of 20 real packages and rejects seeded authorization defects.
• An Agda code generator that turns a DAR into Agda modules, with a proof that they match the decoded package.
• Interfaces, non-unique contract keys, a dpm component, a trace format other tools can compare against, and a tutorial.
• Proofs on Splice code covering authorization, Canton Coin issuance, the CIP-0098 reward cap and the CIP-0105 lock schedule, with a plain-language report.

Part of the grant pays on outside adoption: other teams using the semantics in their own public tests or audit reports.

Obsidian has used Agda on a client’s production Daml system to prove that an optimized code path computes the same results as the code it replaced. Those proofs stopped at the Daml and Canton boundary because no formal model of Daml-LF existed.

We’re looking for a Champion from the Tech & Ops Committee and a technical reviewer. If you build or audit Daml analysis tools, tell us what you would test against it. Alexandre Oliveira wrote the proposal and is happy to do a walkthrough. We can share the draft with a prospective champion.