aeneas
aeneas copied to clipboard
AeneasVerif
A verification toolchain for Rust programs
In , we can see this proof code: ```lean have := AVLNode.update_height_spec a h left_right right progress keep Hupdate₁ with AVLNode.update_height_spec as ⟨ t_new₁, H₁ ⟩ ``` This is a...
We need to add support for mutually recursive trait declarations in Aeneas. In the meantime, we should add a span to the error message.
Companion PR of https://github.com/AeneasVerif/charon/pull/174 Propagates the renaming of meta into span_meta to Aeneas.
Similarly to what is done in Charon, we should add negative tests to Aeneas, for instance to ensure to catch and test unsupported features. One example is #166, where it...
This is a first sketch of user documentation for Aeneas to prove things with Lean. This adds a factorial example with Alectryon and scaffolding from the Lean original project.
Given ```rust pub fn doit(x : usize) -> usize { !x } ``` Running ``` charon --print-llbc``` yields ``` # Final LLBC before serialization: fn bang_vs_not::doit(@1: usize) -> usize {...
`progress with X` where X can now be a full term, e.g. `X := (@SomeSpec.XYZ T U)`. TODO: - [x] diagnose what happens with `as` and some failures - [x]...
> We would be interested in having an Isabelle backend Hi all! @RaitoBezarius pointed me here a while ago. Originally I was interested in using aeneas to maybe try and...
