Post

Cryspen is excited to announce it has been awarded a grant from the Ethereum Foundation to extend our hax verification toolchain with support for the Lean prover. Watch this space for more on this soon! #FormalVerification #Lean #Rust

With the support of this grant, Cryspen will release a new version of hax that can translate Rust source code to purely functional models in Lean, enabling users to mathematically prove the correctness of their code using the increasingly popular Lean proof assistant.