Interactive theorem provers have been used in a number of impressive formal proofs ranging from the Kepler conjecture to C compilers and operating systems, but much less so in the realm of efficient algorithms. We report on the formal proof of the correctness of a functional formulation of Edmond’s blossom algorithm for maximum matchings. Generally, there are two challenges in verifying an algorithm at an abstract level, i.e. not to verify the implementation. The first is to formulate it in a language that has support for verification. The second is to formally prove the lemmas needed for the algorithm’s correctness argument, which may not all be explicitly stated, let alone proven, in the literature. What sets the blossom algorithm apart from other fundamental algorithms, like Dijkstra’s or Ford-Fulkerson, is that the second of the two aforementioned challenges is much more emphasised in its verification. In particular, the verification of the blossom algorithm needs a subtantial library of formalised graph theory to prove Berge’s lemma and the graph theoretic argument behind the correctness of blossom contraction, which is the main step in the algorithm. This project is in collaboration with Kurt Mehlhorn and Tobias Nipkow.