This is the initial release of the Ethos proof checker. Ethos implements the Eunoia logical framework which is a logical framework targeted at SMT solvers. It allows users to define proof formats and write proofs.
This release of Ethos is associated with the 1.2.0 release of the SMT solver cvc5. It can check the proofs generated by cvc5's native proof format cpc. Ethos and Eunoia have reached a certain level of stability, but they are still under active development.
Development Repository
https://github.com/cvc5/ethos
Documentation
https://github.com/cvc5/ethos/blob/main/user_manual.md