diff --git a/CHANGES.md b/CHANGES.md
index bd3f5e076f03f9c4880322bcaa324d84458e6a1c..3c2441c15cbb52c2e290de1697d063cb0b5e8c97 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,5 +1,16 @@
 ## 0.1.1 (Unreleased)
 
+- Add `verify-json` command for verifying a robustness property via a JSON
+  configuration file.
+- Integration of the [nnenum](https://github.com/stanleybak/nnenum) prover.
+- Add printer for VNN-LIB format for property specification as supported by the
+  `nnenum` prover.
+- Add transformation to translate ONNX format into SMT-LIB format for allowing
+  classic solvers to understand and operate on neural networks.
+- Add verification of datasets for classification tasks in terms of a specific
+  CSV format: each line provides the label in 1st column, and data features in
+  the other columns. Also, add builtin implementations of min-max scaling and
+  z-score normalization for data normalization.
 - Rework the section in `README.md` for obtaining CAISAR in order to mention the
   `opam` package just released.
 
diff --git a/README.md b/README.md
index c75e16870df78c161ba45e83e6718f16fc37462d..25e6008786f7ed95be7921573cbb613f2d306e01 100644
--- a/README.md
+++ b/README.md
@@ -102,13 +102,16 @@ $ caisar config --detect
 
 The following are the provers for which a support is provided in CAISAR:
 
-* PyRAT (to be released)
+* PyRAT
 * [Marabou](https://github.com/NeuralNetworkVerification/Marabou)
+* [nnenum](https://github.com/stanleybak/nnenum)
 * [SAVer](https://github.com/abstract-machine-learning/saver)
 
-Under active development is the support for the [SMT-LIB](https://smtlib.cs.uiowa.edu/) which
-is used by many satisfiability modulo theories solvers (e.g. [Alt-Ergo](https://alt-ergo.ocamlpro.com/),
-[Z3](https://github.com/Z3Prover/z3/wiki), [Colibri](https://colibri.frama-c.com/), etc.).
+Moreover, CAISAR supports the [SMT-LIB](https://smtlib.cs.uiowa.edu/) format
+which is used by many satisfiability modulo theories solvers (e.g.
+[Alt-Ergo](https://alt-ergo.ocamlpro.com/), [cvc5](https://cvc5.github.io/),
+[Z3](https://github.com/Z3Prover/z3/wiki),
+[Colibri](https://colibri.frama-c.com/), etc.).
 
 ## Advanced usage