This is an unofficial reimagining of the Archive of Formal Proofs
A Verified Imperative Implementation of B-Treesby Niels Mündler