diff --git a/lib/licenses.nix b/lib/licenses.nix
index 90c1cc177cb3..4d4a3c1a9544 100644
--- a/lib/licenses.nix
+++ b/lib/licenses.nix
@@ -379,6 +379,11 @@ lib.mapAttrs (n: v: v // { shortName = n; }) rec {
     fullName = "Mozilla Public License 2.0";
   };
 
+  mspl = spdx {
+    spdxId = "MS-PL";
+    fullName = "Microsoft Public License";
+  };
+
   msrla = {
     fullName  = "Microsoft Research License Agreement";
     url       = "http://research.microsoft.com/en-us/projects/pex/msr-la.txt";
diff --git a/pkgs/top-level/dotnet-packages.nix b/pkgs/top-level/dotnet-packages.nix
index c0a7adb1d7f8..c3d8b861c767 100644
--- a/pkgs/top-level/dotnet-packages.nix
+++ b/pkgs/top-level/dotnet-packages.nix
@@ -220,6 +220,37 @@ let self = dotnetPackages // overrides; dotnetPackages = with self; {
 
   # SOURCE PACKAGES
 
+  Boogie = buildDotnetPackage rec {
+    baseName = "Boogie-unstable";
+    version = "2017-01-03";
+
+    src = fetchFromGitHub {
+      owner = "boogie-org";
+      repo = "boogie";
+      rev = "5e42f0dd2891b2b85a9198052e55592a2943b7ef";
+      sha256 = "1mjnf96hbn9abgzyvmrfxlhnm213290xb9wca7rnnl12i4fa4ahl";
+    };
+
+    buildInputs = [ dotnetPackages.NUnitRunners ];
+
+    xBuildFiles = [ "Source/Boogie.sln" ];
+
+    outputFiles = [ "Binaries/*" ];
+
+    postInstall = ''
+        mkdir -pv "$out/lib/dotnet/Boogie"
+        ln -sv "${pkgs.z3}/bin/z3" "$out/lib/dotnet/Boogie/z3.exe"
+    '';
+
+    meta = with stdenv.lib; {
+      description = "An intermediate verification language";
+      homepage = "https://github.com/boogie-org/boogie";
+      license = licenses.mspl;
+      maintainers = [ maintainers.taktoa ];
+      platforms = with platforms; (linux ++ darwin);
+    };
+  };
+
   Deedle = buildDotnetPackage rec {
     baseName = "Deedle";
     version = "1.2.0";