diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 338d75b56ab..a16ecc797be 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -16986,6 +16986,8 @@ with pkgs;
 
   ### SCIENCE/PROGRAMMING
 
+  dafny = dotnetPackages.Dafny;
+
   plm = callPackage ../applications/science/programming/plm { };
 
   ### SCIENCE/LOGIC
@@ -17000,6 +17002,8 @@ with pkgs;
 
   aspino = callPackage ../applications/science/logic/aspino {};
 
+  boogie = dotnetPackages.Boogie;
+
   coq_8_3 = callPackage ../applications/science/logic/coq/8.3.nix {
     make = pkgs.gnumake3;
     inherit (ocamlPackages_3_12_1) ocaml findlib;
diff --git a/pkgs/top-level/dotnet-packages.nix b/pkgs/top-level/dotnet-packages.nix
index c3d8b861c76..30267a5ad96 100644
--- a/pkgs/top-level/dotnet-packages.nix
+++ b/pkgs/top-level/dotnet-packages.nix
@@ -221,8 +221,9 @@ let self = dotnetPackages // overrides; dotnetPackages = with self; {
   # SOURCE PACKAGES
 
   Boogie = buildDotnetPackage rec {
-    baseName = "Boogie-unstable";
+    baseName = "Boogie";
     version = "2017-01-03";
+    name = "${baseName}-unstable-${version}";
 
     src = fetchFromGitHub {
       owner = "boogie-org";
@@ -238,8 +239,8 @@ let self = dotnetPackages // overrides; dotnetPackages = with self; {
     outputFiles = [ "Binaries/*" ];
 
     postInstall = ''
-        mkdir -pv "$out/lib/dotnet/Boogie"
-        ln -sv "${pkgs.z3}/bin/z3" "$out/lib/dotnet/Boogie/z3.exe"
+        mkdir -pv "$out/lib/dotnet/${baseName}"
+        ln -sv "${pkgs.z3}/bin/z3" "$out/lib/dotnet/${baseName}/z3.exe"
     '';
 
     meta = with stdenv.lib; {
@@ -251,6 +252,51 @@ let self = dotnetPackages // overrides; dotnetPackages = with self; {
     };
   };
 
+  Dafny = buildDotnetPackage rec {
+    baseName = "Dafny";
+    version = "1.9.8";
+
+    src = fetchurl {
+      url = "https://github.com/Microsoft/dafny/archive/v${version}.tar.gz";
+      sha256 = "0n4pk4cv7d2zsn4xmyjlxvpfl9avq79r06c7kzmrng24p3k4qj6s";
+    };
+
+    preBuild = ''
+      ln -s ${pkgs.z3} Binaries/z3
+    '';
+
+    buildInputs = [ Boogie ];
+
+    xBuildFiles = [ "Source/Dafny.sln" ];
+    xBuildFlags = [ ];
+
+    outputFiles = [ "Binaries/*" ];
+
+    # Do not wrap the z3 executable, only dafny-related ones.
+    exeFiles = [ "Dafny*.exe" ];
+
+    # Dafny needs mono in its path.
+    makeWrapperArgs = "--set PATH ${mono}/bin";
+
+    # Boogie as an input is not enough. Boogie libraries need to be at the same
+    # place as Dafny ones. Same for "*.dll.mdb". No idea why or how to fix.
+    postFixup = ''
+      for lib in ${Boogie}/lib/dotnet/${Boogie.baseName}/*.dll{,.mdb}; do
+        ln -s $lib $out/lib/dotnet/${baseName}/
+      done
+      # We generate our own executable scripts
+      rm -f $out/lib/dotnet/${baseName}/dafny{,-server}
+    '';
+
+    meta = {
+      description = "A programming language with built-in specification constructs";
+      homepage = "http://research.microsoft.com/dafny";
+      maintainers = with maintainers; [ layus ];
+      license = licenses.MIT;
+      platforms = with platforms; (linux ++ darwin);
+    };
+  };
+
   Deedle = buildDotnetPackage rec {
     baseName = "Deedle";
     version = "1.2.0";