  We establish that every monadic second-order logic (MSO) formula on graphs
with bounded treedepth is decidable in a constant number of rounds within the
CONGEST model. To our knowledge, this marks the first meta-theorem regarding
distributed model-checking. Various optimization problems on graphs are
expressible in MSO. Examples include determining whether a graph $G$ has a
clique of size $k$, whether it admits a coloring with $k$ colors, whether it
contains a graph $H$ as a subgraph or minor, or whether terminal vertices in
$G$ could be connected via vertex-disjoint paths. Our meta-theorem
significantly enhances the work of Bousquet et al. [PODC 2022], which was
focused on distributed certification of MSO on graphs with bounded treedepth.
Moreover, our results can be extended to solving optimization and counting
problems expressible in MSO, in graphs of bounded treedepth.
