Formal Verification

As far as I figured out it is possible to do Formal Verification on DAML.
I’m curious how this is done. Are there any practical examples?

Hi Qohelet, in fact, this is something that we’re currently working on!

Concretely, we’re developing a rather specialized form of formal verification for DAML, where the compiler verifies whether a certain choice always preserves the total amount of given field. This way, the programmer would be warned statically when his choice definition could potentially burn or create cash out of thin air.

The main advantage of a specialized approach like this, is that the static analysis can run automatically and fast, without requiring user interaction.

Please note that, at the moment, this is still very much a work in progress. But you can expect a blog post about this topic (with some examples) very soon!

Said blogpost: What is Formal Verification and what it means for DAML - DAML.

this is a great blog post on formal verification tool , thanks for sharing @Gary_Verhaegen. Let us know if you have further questions @Qohelet.