binomial_heap_proof It is a great project that tries to prove the correctness of binomial heap both in C and coq.