Paxos consensus algorithm implemented in the functional validation language Dafny
Get the latest version of Dafny. The compiler does not require a setup process and you may simply extract the zip somewhere befitting. If you have Visual Studio 2010 or newer installed you may also install the Dafny Language Extension by opening the file DafnyLanguageService.vsix
Open paxos.dfy with Dafny.exe or dfy-compile.bat. If dfy-compile.bat can't find Dafny.exe, run it once without arguments where it can find it and add it to the %PATH% system variable. After this, dfy-compile.bat can be used from anywhere.
Notes: Dafny runs in a .NET environment. Make sure you have .NET Framework 4 installed
Download and install Mono.
Get the latest version of Dafny. Install (unzip) Dafny to a suitable folder (e.g. inside the Paxos-in-Dafny folder).
Get the Z3 theorem prover. Unzip the Z3 folder inside the Dafny folder. Make a symbolic link to the z3.exe file from the Dafny folder (where the Dafny.exe file resides). This is so that Dafny can find Z3.
Open a terminal window and run:
cd Paxos-in-Dafny
mono Dafny/Dafny.exe paxos.dfy