In my first year internship at the MPRI I worked with the EPI Prosecco team at Inria Paris on proof automation in the specific context of verification of cryptographic algorithms. In particular, I worked on developing a verified implementation of the SHA3 family of functions in Rust, verified in Lean.

The code of this effort can be found on github. The implementation does not make use of any loop unrolling or specific vectorized instructions, but it does represent the Keccak permutation function's state using packed machine integers, for efficiency.