diff --git a/pkgs/applications/science/logic/easycrypt/default.nix b/pkgs/applications/science/logic/easycrypt/default.nix
index 5f28ca73c4e..da4ff212e29 100644
--- a/pkgs/applications/science/logic/easycrypt/default.nix
+++ b/pkgs/applications/science/logic/easycrypt/default.nix
@@ -1,4 +1,4 @@
-{ lib, stdenv, fetchFromGitHub, ocamlPackages, why3 }:
+{ lib, stdenv, fetchFromGitHub, fetchpatch, ocamlPackages, why3 }:
 
 stdenv.mkDerivation rec {
   pname = "easycrypt";
@@ -11,6 +11,12 @@ stdenv.mkDerivation rec {
     sha256 = "sha256:09rdwcj70lkamkhd895p284rfpz4bcnsf55mcimhiqncd2a21ml7";
   };
 
+  # Fix build with Why3 1.5
+  patches = fetchpatch {
+    url = "https://github.com/EasyCrypt/easycrypt/commit/d226387432deb7f22738e1d5579346a2cbc9be7a.patch";
+    sha256 = "sha256:1zvxij35fnr3h9b5wdl8ml17aqfx3a39rd4mgwmdvkapbg3pa4lm";
+  };
+
   nativeBuildInputs = with ocamlPackages; [
     dune_3
     findlib
diff --git a/pkgs/applications/science/logic/why3/default.nix b/pkgs/applications/science/logic/why3/default.nix
index 0f3dab8038e..8917135b2c8 100644
--- a/pkgs/applications/science/logic/why3/default.nix
+++ b/pkgs/applications/science/logic/why3/default.nix
@@ -3,11 +3,11 @@
 
 stdenv.mkDerivation rec {
   pname = "why3";
-  version = "1.4.1";
+  version = "1.5.0";
 
   src = fetchurl {
     url = "https://why3.gitlabpages.inria.fr/releases/${pname}-${version}.tar.gz";
-    sha256 = "sha256:1rqyypzlvagrn43ykl0c5wxyvnry5fl1ykn3xcvlzgghk96yq3jq";
+    sha256 = "sha256:0qjh49pyqmg3xi09fn4lyzz23i6h18y9sgc8ayscvx3bwr3vcqhr";
   };
 
   buildInputs = with ocamlPackages; [
diff --git a/pkgs/applications/science/logic/why3/with-provers.nix b/pkgs/applications/science/logic/why3/with-provers.nix
index ae0acb1e525..739064bb616 100644
--- a/pkgs/applications/science/logic/why3/with-provers.nix
+++ b/pkgs/applications/science/logic/why3/with-provers.nix
@@ -27,6 +27,6 @@ stdenv.mkDerivation {
 
   installPhase = ''
     mkdir -p $out/bin
-    makeWrapper ${why3}/bin/why3 $out/bin/why3 --add-flags "--extra-config $out/share/why3/why3.conf"
+    makeWrapper ${why3}/bin/why3 $out/bin/why3 --add-flags "--config $out/share/why3/why3.conf"
   '';
 }
diff --git a/pkgs/development/tools/analysis/frama-c/default.nix b/pkgs/development/tools/analysis/frama-c/default.nix
index b5ae5055d02..0b962a97ef1 100644
--- a/pkgs/development/tools/analysis/frama-c/default.nix
+++ b/pkgs/development/tools/analysis/frama-c/default.nix
@@ -4,6 +4,15 @@
 , gdk-pixbuf, wrapGAppsHook
 }:
 
+let why3_1_5 = why3; in
+let why3 = why3_1_5.overrideAttrs (o: rec {
+  version = "1.4.1";
+  src = fetchurl {
+    url = "https://why3.gitlabpages.inria.fr/releases/${o.pname}-${version}.tar.gz";
+    sha256 = "sha256:1rqyypzlvagrn43ykl0c5wxyvnry5fl1ykn3xcvlzgghk96yq3jq";
+  };
+}); in
+
 let
   mkocamlpath = p: "${p}/lib/ocaml/${ocamlPackages.ocaml.version}/site-lib";
   runtimeDeps = with ocamlPackages; [