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

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]. [0] https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf https://lamport.azurewebsites.net/tla/formal-methods-amazon.... [1] https://learntla.com/ https://learntla.com/