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: The certificate checker is not yet fully verified, and likely contains bugs. Currently, only certificates without latches are supported, but this covers IC3 proofs. 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