What's the status of Daml Drivers (ie. runtimes) with respect to formal verification?

Quesiton from a presentation. Has anything been formally verified in the drivers?

The driver implementations themselves have not been analyzed formally. We have done some steps towards formally verifying the underlying high-level concepts, e.g., Merkle trees and some properties of the Daml ledger model. The results are published on the research page for Canton.

Also a relevant blogpost here:

DAML Formal Verification News

DAML Community , here @gertjanb wrote a great blog post on Formal Verification & DAML. Topics such as: What is Formal Verification? Formal Verification in DAML How the demo works What is the Future of Formal Verification in DAML? Formal Verification FAQ check it out [Formal Verification DAML] Comment here if you have any questions for @gertjanb!