@Andreas_Lochbihler and myself have a new paper on formally modelling Merkle trees and similar so-called “authenticated data structures” in the theorem prover Isabelle. Such structures allow several systems to ensure that they’re talking about the same structure, even if everyone has only a part of the structure.
Yes but why? The reason for the exercise are DAML transactions; there, you can have parties and participant nodes that only see a part of the transaction (their “projections”), but we still want the transaction to commit atomically. So this is a first step towards formally modelling distributed commit protocols (wink: maybe even distributed across multiple ledgers? who knows!) for DAML transactions that maintain the privacy properties of the DAML ledger model.