aeneas
aeneas copied to clipboard
AeneasVerif
A verification toolchain for Rust programs
The Makefiles are getting bloated in particular when it comes to the test generation, and are probably not the best way of managing a project like Aeneas today. It would...
For now, the definitions supported by our standard libraries are hardcoded in `ExtractBuiltin.ml`. This information should be moved to an external file which should be read at runtime.
The formatting of some code blocks is not always pretty and in particular indentation is sometimes weird (for instance, the indentation of the `do ...` blocks in Lean). Also, it...
We should improve the formatting functions (in `Print.ml` for instance). In particular, we should use the `Format` or `PPrint` module instead of directly generating string (the indentations and the breaklines...
We could turn Aeneas into a borrow checker by printing informative error messages when there is a borrow checking error (or more generally speaking an invalid access, in particular to...
Some definitions in the various backends have admits