Modeling FO-limits for monadically stable sequences

We show that given a monadically stable theory $T$, a sufficiently saturated $\mathbf{M}\models T$, and a coherent system of probability measures on the $\sigma$-algebras generated by parameter-definable sets of $\mathbf{M}$ in each dimension, we may produce a totally Borel $\mathbf{B}\prec \mathbf{M}$ realizing these measures. Our main application is to prove that every FO-convergent sequence of structures (with countable signature) from a monadically stable class admits a modeling limit. As another consequence, we prove a Borel removal lemma for monadically stable Lebesgue relational structures.