Fantastic stuff! For all those folks who liked PropCheck.jl (which is just a fancy fuzzer), this is the mathematically correct theorem proving counterpart!
Do you have plans for depending (weakly) on Z3.jl or other solvers like cvc5, so that users don’t have to install the solver through their system package manager and instead can just use a JLL from Pkg?
As for the name - I think it’s fine, since this is more or less an interface package. Kind of like Tables.jl is an interface package.