Formosa Keccak is a formally verified implementation of Keccak and related functions (SHA3, SHAKE, etc.).
