Valaig is a framework for efficient And-Inverter Graph (AIG) manipulation and reasoning in Lean, with a verified checker for the certifaiger model checking certificate format.
This requires Lean 4, easily installed through the elan toolchain. To build all Valaig tools:
lake buildNOTE: Although the checker has been verified, the parser is not and likely contains bugs. Currently, only certificates with a single bad property and no constraints are supported. You can generate and check a certificate with rIC3 as follows:
ric3 check --cert certificate.aig problem.aig ic3
lake exe valaigcert problem.aig certificate.aig