Abstract We introduce an updated version of the Pono model checker. Pono is a versatile SMT-based model checker that integrates multiple verification algorithms and interfaces with a wide range of SMT solvers through a solver-agnostic back end. It emphasizes usability, offering support for commonly used input formats and providing C++ and Python APIs for programmatic access. The new version 2.0 introduces several important new features, including support for liveness properties, new interpolation-based safety-checking engines, a new VMT-LIB front end, and a number of usability and performance enhancements. An evaluation of the new version demonstrates significant improvements in performance over its previous version and comparable performance to other state-of-the-art model checkers. These results highlight Pono 2.0’s effectiveness as a general-purpose and easily extensible verification platform.