$\texttt{markovml}$: A Python Package for Verifying Markov Processes with Embedded Machine Learning Models

We present $\texttt{markovml}$, a Python package for verifying properties of Markov processes whose parameters are defined by machine learning (ML) models. While existing tools support formal verification of either Markov processes or ML models individually, none support reasoning about systems that integrate both. $\texttt{markovml}$ fills this gap by allowing users to construct Markov processes and embed pretrained models from standard ML libraries, including linear models, decision trees, and neural networks. The package provides an expressive domain-specific language to specify constraints and verify common properties such as reachability, expected hitting time, and total reward. We illustrate usage through several examples and release the package with full documentation and tutorials.