A case study with Aeneas and jxl-rs

This blog post by Jonathan Protzenko discusses Aeneas, a toolchain for verifying Rust programs, and showcases recent improvements and how to proof code effectively using Aeneas. It serves as both a case study and a tutorial based on a real-world programming example.