Developer-driven Rust verification using hax, Lean, and AI
Showcasing hax 0.4 on IoT-friendly SHA-3
As announced in our recent blog post, hax 0.4 has a new Lean backend that relies on Aeneas. In this post, we describe how we used this new backend to verify the SHA-3 implementation in libcrux-iot, an …
