Microservices Architecture is a popular pattern used for building complex IT systems in an incremental, sustainable and scalable fashion. However, compared with traditional monolithic solution architectures, it introduces a higher degree of concurrency which might result in subtle bugs arising, such as race conditions, deadlocks and lack of data consistency. I shall illustrate this with a worked example of an automated insurance claims payment service which exhibits a bug whereby a particular claim may be settled twice. I shall use the CSP formal modelling language and the FDR refinement checker to prove some results about this bug and how to fix it.