-
Notifications
You must be signed in to change notification settings - Fork 1
Tool carcara
Bruno Andreotti, Haniel Barbosa.
Carcara is a proof checker and elaborator for Alethe proofs.
Carcara is an efficient, usable, and independent checker and elaborator for SMT proofs in the Alethe format. It was developed in the Rust programming language, and is available both as a command line program and as a Rust API.
Carcara is open-source, and available on GitHub: https://github.com/ufmg-smite/carcara
The checker has support for all rules defined in the Alethe format documentation, and is able to check Alethe proofs produced by both the veriT and cvc5 SMT solvers. Carcara is under active development, receiving new features and improvements, and following the Alethe format as it evolves.
Besides checking a proof, Carcara also has support for elaboration: this is the process of taking a proof that contains coarse-grained steps and breaking them down into more detailed, finer-grained steps, outputting a new proof that is (in theory) easier to check.
There is ongoing work to implement parellel proof checking in Carcara. Since the steps in a proof are in general independent, it is in theory possible to check them in parallel.
Given an SMT-LIB problem and an Alethe proof, you can check it by running:
carcara check example.smt2.proof example.smt2
The tool will print valid if the proof is valid and complete, holey if it is valid but contains
holes, and invalid if it is not valid, together with a helpful error message.
You can elaborate a proof with:
carcara elaborate example.smt2.proof example.smt2
Carcara will check the proof and elaborate it, printing the elaborated proof if no errors were found.
See the repository for more information.
The official repository of the tool.
The documentation of the Alethe format.
Bruno Andreotti, Hanna Lachnitt, and Haniel Barbosa. Carcara: An efficient proof checker and elaborator for SMT proofs in the alethe format. Proceedings of the 29th Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'23), Paris, France, Volume 13994 of LNCS. Springer, 2023. DOI: https://doi.org/10.1007/978-3-031-30823-9_19