rem-verifyer

This is a toolchain that allows for two .llbc files (generated by CHARON) to be compared for equivalence. This is done using CoQ. The files are converted to CoQ using AENEAS, and the given method(s) are proved to be equivalent through an automatically generated and run proof.

It is important to note that this module has no way to generate the .llbc files. That must be handled externally (i.e. by a standalone install of CHARON or by the rem-cli/(command) tool). At this stage, AENEAS seems to work best on Linux, so it is recommeded to run the program on a Linux machine. It is a WIP to get it working on Windows and MacOS/other UNIX systems.

Requirements:

• CoQ (version 8.18.0)
• AENEAS (https://github.com/AeneasVerif/aeneas)