For my bachelor research project, supervised by Bas Luttik, I set out to verify Aravind’s bounded least recently used (BLRU) algorithm for mutual exclusion using mCRL2. An interesting property of Aravind’s algorithm is that it can ensure mutual exclusion even when the registers used are safe, rather than atomic. In order to verify this property, I modelled the behavior of safe registers in mCRL2. I will present this model, and show the effects of safe registers by demonstrating how Peterson’s algorithm violates mutual exclusion when safe registers are used. I will also discuss the results of verifying Aravind’s algorithm.