Cryptography in Lean 4
This repo contains some experiments that are progressing to specifications of AES, SHA3 and Classic McEliece in Lean.
Please contact me if you are interested in working on cryptographic specifications in Lean.
joehendrix/lean-crypto
Cryptographic routines for the Lean 4 language
GitHub Link DocumentationPick a version!
TODO: should show a time axes that allows the users to view, filter and click copy the lakefile config.