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.
2 Likes
Also a relevant blogpost here: