This repository contains a fully verified Merkle Tree, with a proof by security reduction to a collision to the underlying hash function.
We demonstrate how to build a project on top of EverCrypt by only using the "public" APIs and a minimal build burden.