A case study with Aeneas and jxl-rs

Aeneas is a toolchain for verifying Rust programs, relying on a functional translation to Lean. Aeneas is now nearly five years old, and many excellent improvements have landed recently, thanks to the work of Son Ho, Aymeric Fromherz, Guillaume Boisseau and many other collaborators. With this blog post, I’m hoping to showcase how proofs in Aeneas look like these days, and highlight recent improvements, by relying on a sample problem given to me by my colleague Luca Versari. I think this blog post can also serve as a nice example / tutorial on how to work with Aeneas on a real-world piece of code. Before going any further: more info about Aeneas is available on GitHub, and most communication happens on our Zulip – subscribe to the newsletter channel there if you’d like to stay updated. Finally, the science is in our ICFP’22 and ICFP’24 papers. Background: jxl-rs jxl-rs is a rewrite of the jpeg-xl codec, in Rust. For performance reasons, parts of the rewrite do rely on unsafe code. In…