In this repository, formal methods are used to model the "Lamport Bakery" using an invented language. The invented language has variables, loops, conditional instructions and even arrays.
The code is based on Maude, which is a language for formal specification.
http://maude.cs.illinois.edu/w/index.php/The_Maude_Project_and_Team
This repository was made with the help of a colleague and my university tutor at the time.
From Wikipedia: Lamport's bakery algorithm is a computer algorithm devised by computer scientist Leslie Lamport, as part of his long study of the formal correctness of concurrent systems, which is intended to improve the safety in the usage of shared resources among multiple threads by means of mutual exclusion.