Formal verification works on Bitcoin precisely because Script is so constrained. No loops, no mutable state, just a stack-based predicate language. Miniscript already gives you compositional reasoning over spending conditions. The boringness isn't a limitation, it's what makes the proof tractable. You can't formally verify a system whose rules change at the discretion of a committee.