This reminds me of an article I read a while ago https://alastairreid.github.io/mrs-at-scale/

MRSs would enable much more of the formal verification parts to be generated.