The decisions made by software architects can have significant repercussions if they are made incorrectly. Therefore, it is crucial to base such decisions on concrete evidence rather than solely relying on heuristic experiences to determine if the architectural design decisions were correct. This approach can help avoid incurring refactoring or reengineering costs in the future. This work proposes a general model for the formal verification of software architectures and presents a case study of an architecture based on microservices for ensuring high availability. Through this thesis, the different steps of the model will be presented, and it will be demonstrated how they should be applied to carry out a formal verification. This verification can guide software architects in making decisions based on formal evidence using automatic verification tools.