diff --git a/NEWS.md b/NEWS.md new file mode 100644 index 0000000..e0f47d4 --- /dev/null +++ b/NEWS.md @@ -0,0 +1,17 @@ +This file contains a summary of important user-visible changes. + +ethos 0.1.0 +=========== + +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 +