Lambda
Lambda is a model checker for the safety of parameterized transition systems. The state variables are functions from uninterpreted sorts into Booleans, integers, reals or enumerations, and the formulae describing the system can quantify over the uninterpreted sorts. Lambda tries to prove that a safety property holds for all cardinalities of the sorts, or to find a counterexample.
The input language is an extension of VMT-LIB. When the property holds, Lambda produces an inductive invariant that can be checked independently with SMT solvers such as Z3 or cvc5, or in Lean.