rreview cryptography implemeentation in the project proivide me a formal verification in coq thsat it actually work as inteneded make sure all codebased is test covered