📝 DAML Formal Verification

DAML Community ,
:right_anger_bubble: here @gertjanb wrote a great blog post on Formal Verification & DAML.

Topics such as:
:arrow_right: What is Formal Verification?
:arrow_right: Formal Verification in DAML
:arrow_right: How the demo works
:arrow_right: What is the Future of Formal Verification in DAML?
:arrow_right: Formal Verification FAQ

check it out :point_down:

Comment here if you have any questions for @gertjanb!


Great post! I hadn’t seen the IDE integration yet.

I was wondering why we decided to use annotations instead of Scenario or Script-like approach?

Do you think there are any disadvantages to coupling these assertions to the template, instead of allowing them to be tested independelty?

1 Like

Note that the IDE integration does not yet exist neither do the annotations. At the moment, the UX is a command line tool that you pass in the name of the choice and the name of the field you want to verify.

I think it’s perfectly feasible to allow for more expressive assertions in the future but we had to start somewhere :slightly_smiling_face:


I was wondering if there’s progress on this.


Hi @jvelasco.intellecteu, there haven’t been any changes since then.