Most people associate "blockchains" with a protocol by which the "blocks" are inserted. Usually these things revolve around proof-of-work, proof-of-stake, proof-of-space, fairness criteria, etc. I think everyone gets that the Guardtime product is hashtree. From a formal verification perspective, the critical behavior is probably in the protocol, and most likely not the implementation of the datastructure or database.