What do you mean by model checking? Usually anything with the keyword "Design" like design patterns for microservices have no science or mathematics to back it up.
You may be technically correct, but I'd argue it's generally more useful what we do have: practical experience. When one says "we need better architects", to me that implies that our current architects are creating design patterns and reference implementations that are both 1) not practical, and 2) don't adhere to known-good best practices.
Systems design in real life is an "artistic science": there are always known limitations (and some expected unknown ones) that rule out the theoretic optimal design for good reasons. The problem is that limitations and compromises are often not disclosed, and that many programmers and architects are too inexperienced to really grok the implicit meaning behind specific design decisions.
So we struggle along, with bloggers, researchers and FOSS contributors halfheartedly collaborating to make point improvements as solutions are discovered. Stodgy enterprises suffer, big tech companies make decisions with global impact, startups are left wondering WTF to do, and the rest of us largely don't care. Why? Because nit picking doesn't solve business problems [almost ever. I'd argue this point in cases of things like SCADA systems and other mission critical control systems.].
The thing with practical experience is you can put two engineers with practical experience in a room and they can argue for days about a architecture or design pattern.
Nobody argues about which algorithm is better for sorted data sets: linear search or binary search. Theory already establishes one is faster than the other, but no theory establishes which architecture is better than the other.
A model checker is a software program you use to validate a given mathematical model of a system. If the proposed properties of the model hold the model checker will let you know. More interestingly if the properties fail to hold you'll get a trace back into where your assumptions fell apart.
TLA+ is one such system that includes a language for writing models and a model checker to verify them for you. In the context of microservices you would write a model of your services and the checker would help you to verify that certain properties of your model will hold for all possible executions of the model. Properties people seem to be interested in are consistency and transaction isolation. You can develop a model of your proposed microservices architecture and work out the errors in your design before you even write a lick of code.
Or if you already have a microservice system you could write a model of it and find if there are flaws in its design causing those annoying error reports.
Amazon wrote a paper about how they use it within the AWS team [0]. Highly worth the read. And if any of this sounds interesting I suggest checking out Hillel Wayne's course he's building [1].
I'll take a TLA+ specification over a diagram any day.