Go to the "Download" tab (to the right, or use the Downloads tab above) and click on the current release to download a zip file containing all of the binaries you need to run Boogie (and Dafny). Please let us know if something doesn't work!
After you download the Boogie zip file, you'll need to tell Windows to unblock its contents. To do that, right-click on the zip file, select Properties, click the Unblock button, and click OK. You can then unzip the contents into the folder of your choice.
You need some underlying prover to run Boogie. We recommend Z3 (of which you'll need version 3.2 or later), see the Z3 page
for download/installation information. Note, Boogie will find Z3 if you install it according to the default settings in the Z3 installer. However, if you have a copy of z3.exe in the Boogie binaries directory, Boogie will prefer that copy. You can use Boogie's /trace flag to see where Boogie is getting Z3 from, and there are also command-line flags for letting you specify a different location (see /help).
The Boogie zip file also contains Dafny. However, it does not include the Dafny mode for Visual Studio. To install the Dafny mode for Visual Studio, you need to build from sources
Apparently some people persist in using a 1970s operating system. If you are one of those unfortunate people, then Zvonimir Rakamaric
has written a tutorial
on how to run Boogie under Linux.NOTE
: The new bytecode translator is not
included in the binary release. It will be once it is fully functional.