  MoXI is a new intermediate verification language introduced in 2024 to
promote the standardization and open-source implementations for symbolic model
checking by extending the SMT-LIB 2 language with constructs to define
state-transition systems. The tool suite of MoXI provides a translator from
MoXI to Btor2, which is a lower-level intermediate language for hardware
verification, and a translation-based model checker, which invokes mature
hardware model checkers for Btor2 to analyze the translated verification tasks.
The extensibility of such a translation-based model checker is restricted
because more complex theories, such as integer or real arithmetics, cannot be
precisely expressed with bit-vectors of fixed lengths in Btor2. We present
MoXIchecker, the first model checker that solves MoXI verification tasks
directly. Instead of translating MoXI to lower-level languages, MoXIchecker
uses the solver-agnostic library PySMT for SMT solvers as backend for its
verification algorithms. MoXIchecker is extensible because it accommodates
verification tasks involving more complex theories, not limited by lower-level
languages, facilitates the implementation of new algorithms, and is
solver-agnostic by using the API of PySMT. In our evaluation, MoXIchecker
uniquely solved tasks that use integer or real arithmetics, and achieved a
comparable performance against the translation-based model checker from the
MoXI tool suite.
