Proof-of-concept for verifying Plonky3 FRI cryptographic code using Aeneas (MIR-based, pure functional extraction) as an alternative to Hax (annotation-driven, monadic extraction). - View it on GitHub