- Author
- Not stated; the AeneasVerif GitHub organization
- Published
- Undated
- Kind
- Open-source project README
- Original
- github.com/AeneasVerif/charon
- Subject
- Formal methods and proof
What it is
The README is published by the AeneasVerif GitHub organization, with no named authors. It presents Charon as the front end for analysis and verification tools. It links to a manual and API documentation.
What it says
- Charon extracts a Rust crate and its dependencies into a JSON file.
- The output holds types, functions, traits, simplified MIR bodies and source information.
- Run charon inside the crate, like cargo build, to get an llbc file.
- The aim is to centralise the work of getting information out of rustc internals.
- The README says Charon suits semantic analyses and likely will not help with lints.
- It describes Charon as beta software with open bugs and planned breaking changes.
What evidence it gives
The README shows the output shape and the build commands. It states the purpose and limits in prose. It gives no benchmarks and no list of tested crates.
Interests and limits
The authors describe their own project. The README was read in full, but the linked manual and limitations page were not. The claim that translation is well tested is not backed here. The page is short and mostly a pointer to other documents.