Formally Verified Cryptography Proofs Using Lean 4
This library is an ongoing port of the work found here, from Lean 3 to Lean 4. All of the basic theory is present here, but some proofs and APIs are still actively being moved.
This library is an ongoing port of the work found here, from Lean 3 to Lean 4. All of the basic theory is present here, but some proofs and APIs are still actively being moved.