Cvc.lean User Manual

Welcome to the cvc.lean user manual. The code documentation is available at anzenlang.io/cvc.lean.

Cvc.lean is a high-level API for the cvc5 SMT solver written by Adrien Champion from anzenlang for the cvc5 team in collaboration with Cesare Tinelli at the University of Iowa.

This library is built on lean-cvc5 and exposes cvc5's terms, solver, term/solver-related functions, and adds (many) more (strongly-typed) features on top such as lean syntax extensions for natural term-construction and symbol/state structures, as well as a transition system API equipped with a k-induction engine.

This user manual is not an introduction to SMT solvers. It assumes readers are familiar with the basics of SMT solving and of the SMT-LIB standard.