#1039 overall
Learn TLA+
learntla.com
1 recommender · 1 thread · recommended in 1 year, 2018 · score 0.7
Learn TLA+ is an online course by Hillel Wayne that teaches TLA+, a formal specification language and model checker for writing models of systems and checking their properties across all possible executions.
Commenters point to it as the way to get started with TLA+ for checking designs such as microservice architectures before writing code.
CS Fundamentals & Systemsbeginnerself-paced text#tla+#formal methods#model checking#specification#wayne
Recommendations by year
20062026
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.... [1] https://learntla.com/