I used to work in this field myself long ago (academically and practically). The difficulty that OP didn't suggest much appreciation for is that the interesting spaces for automated verification -- especially of distributed systems, say -- require exploring the space of formalisms between the trivial proofs of propositional logic (SAT solvers) and the undecidable proofs of first or second-order logic (interactive theorem proving environments such as Isabelle and Lean). This is the incredibly large space occupied most importantly by the various modal logics, which allow for quantification over graph traversals. There are remarkably expressive logics where the decision problem remains tractable, such as the modal mu-calculus.

That is, precisely if one wants automated tools for verification the seemingly obtuse work on novel formal systems is necessary.