VerifiedInsertionSort A functional insertion sort algorithm, formally verified in the Coq interactive theorem prover by Inria. Written somewhere around 2021/2022.