Formalization of the GCL language and associated semantics and analysis in Lean 4. Based on the book Formal Methods: An Appetizer by Flemming Nielson and Hanne Riis Nielson.
To build the project, one needs to install Lean. The recommended approach is to use VS Code as listed here. If you prefer the CLI, install elan and run lake build.