on the occasion of the 68th birthday of the Flag or Europe, we are delighted to release the version 1.0 of CAISAR. The release source is available under our gitlab. You can install it via opam with
opam install caisar.
We also have a docker image hosted on Dockerhub packaging CAISAR and some dedicated provers. You can pull it with
docker pull laiser/caisar:pub.
We extended the WhyML specification language to take into account common machine learning constructs. It is now possible to model machine learning computations using vectors and datasets. Parts of this specification can be interpreted directly by CAISAR. CAISAR can then instanciate the specification with concrete values provided by the user. CAISAR can also compute the results of operations on vectors such as getting an index on a concrete vector, or normalizing a dataset. Finally, this language allows to perform transformations on the proof goals that makes them more amenable for provers.
The end result is a cleaner modelling language that behaves “as expected” for the user, bridging the gap between the specification and the actual system to verify. We believe that this will surely be helpful for the community.
Check the updated documentation examples to get a grasp on the new language.
It is now possible to specify which theories and/or goals to check within a specification. CAISAR is now available as a Nix flake. We plan to make it available on nixpkgs in a future release. We added a contribution guide in the manual, under the “Contributing” section.
Merry end-of-year celebrations!