diff --git a/pkgs/applications/science/logic/why3/configure.patch b/pkgs/applications/science/logic/why3/configure.patch
new file mode 100644
index 00000000000..3eebf3cf165
--- /dev/null
+++ b/pkgs/applications/science/logic/why3/configure.patch
@@ -0,0 +1,11 @@
+diff --git a/configure b/configure
+--- a/configure
++++ b/configure
+@@ -4029,7 +4029,6 @@ fi
+ 
+ if test "$USEOCAMLFIND" = yes; then
+    OCAMLFINDLIB=$(ocamlfind printconf stdlib)
+-   OCAMLFIND=$(which ocamlfind)
+    if test "$OCAMLFINDLIB" != "$OCAMLLIB"; then
+    USEOCAMLFIND=no;
+    echo "but your ocamlfind is not compatible with your ocamlc:"
diff --git a/pkgs/applications/science/logic/why3/default.nix b/pkgs/applications/science/logic/why3/default.nix
index a3b369ad54a..bd538dc6c75 100644
--- a/pkgs/applications/science/logic/why3/default.nix
+++ b/pkgs/applications/science/logic/why3/default.nix
@@ -1,4 +1,5 @@
-{ fetchurl, stdenv, ocamlPackages, coq }:
+{ callPackage, fetchurl, stdenv
+, ocamlPackages, coqPackages, rubber, hevea, emacs }:
 
 stdenv.mkDerivation rec {
   name    = "why3-${version}";
@@ -9,14 +10,34 @@ stdenv.mkDerivation rec {
     sha256 = "0xz001jhi71ja8vqrjz27v63bidrzj4qvg1yqarq6p4dmpxhk348";
   };
 
-  buildInputs = (with ocamlPackages; [
-      ocaml findlib num lablgtk ocamlgraph zarith menhir ]) ++
-    stdenv.lib.optionals (ocamlPackages.ocaml == coq.ocamlPackages.ocaml ) [
-      coq ocamlPackages.camlp5
-    ];
+  buildInputs = with ocamlPackages; [
+    ocaml findlib ocamlgraph zarith menhir
+    # Compressed Sessions
+    # Emacs compilation of why3.el
+    emacs
+    # Documentation
+    rubber hevea
+    # GUI
+    lablgtk
+    # WebIDE
+    js_of_ocaml js_of_ocaml-ppx
+    # Coq Support
+    coqPackages.coq coqPackages.flocq ocamlPackages.camlp5
+  ];
+
+  propagatedBuildInputs = with ocamlPackages; [ camlzip num ];
+
+  enableParallelBuilding = true;
+
+  # Remove unnecessary call to which
+  patches = [ ./configure.patch ];
+
+  configureFlags = [ "--enable-verbose-make" ];
 
   installTargets = [ "install" "install-lib" ];
 
+  passthru.withProvers = callPackage ./with-provers.nix {};
+
   meta = with stdenv.lib; {
     description = "A platform for deductive program verification";
     homepage    = "http://why3.lri.fr/";
diff --git a/pkgs/applications/science/logic/why3/with-provers.nix b/pkgs/applications/science/logic/why3/with-provers.nix
new file mode 100644
index 00000000000..3528dbd3a64
--- /dev/null
+++ b/pkgs/applications/science/logic/why3/with-provers.nix
@@ -0,0 +1,30 @@
+{ stdenv, makeWrapper, runCommand, symlinkJoin, why3 }:
+provers:
+let configAwkScript = runCommand "why3-conf.awk" { inherit provers; }
+    ''
+      for p in $provers; do
+        for b in $p/bin/*; do
+          BASENAME=$(basename $b)
+          echo "/^command =/{ gsub(\"$BASENAME\", \"$b\") }" >> $out
+        done
+      done
+      echo '{ print }' >> $out
+    '';
+in stdenv.mkDerivation {
+  name = "${why3.name}-with-provers";
+
+  phases = [ "buildPhase" "installPhase" ];
+
+  buildInputs = [ why3 makeWrapper ] ++ provers;
+
+  buildPhase = ''
+      mkdir -p $out/share/why3/
+      why3 config --detect-provers -C $out/share/why3/why3.conf
+      awk -i inplace -f ${configAwkScript} $out/share/why3/why3.conf
+  '';
+
+  installPhase = ''
+      mkdir -p $out/bin
+      makeWrapper ${why3}/bin/why3 $out/bin/why3 --add-flags "--extra-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 29a19022094..5f6b894f984 100644
--- a/pkgs/development/tools/analysis/frama-c/default.nix
+++ b/pkgs/development/tools/analysis/frama-c/default.nix
@@ -1,87 +1,77 @@
-{ stdenv, fetchurl, makeWrapper, ncurses, ocamlPackages, graphviz
-, ltl2ba, coq, why3, autoconf
+{ lib, stdenv, fetchurl, makeWrapper, writeText
+, autoconf, ncurses, graphviz, doxygen
+, ocamlPackages, ltl2ba, coq, why3,
 }:
 
 let
   mkocamlpath = p: "${p}/lib/ocaml/${ocamlPackages.ocaml.version}/site-lib";
-  ocamlpath = "${mkocamlpath ocamlPackages.apron}:${mkocamlpath ocamlPackages.mlgmpidl}";
+  runtimeDeps = with ocamlPackages; [
+    apron
+    biniou
+    camlzip
+    easy-format
+    menhir
+    mlgmpidl
+    num
+    ocamlgraph
+    why3
+    yojson
+    zarith
+  ];
+  ocamlpath = lib.concatMapStringsSep ":" mkocamlpath runtimeDeps;
 in
 
 stdenv.mkDerivation rec {
   name    = "frama-c-${version}";
-  version = "18.0";
-  slang   = "Argon";
+  version = "19.0";
+  slang   = "Potassium";
 
   src = fetchurl {
     url    = "http://frama-c.com/download/frama-c-${version}-${slang}.tar.gz";
-    sha256 = "0a88k2mhafj7pz3dzgsqkrc9digkxpnvr9jqq9nbzwq8qr02bca2";
+    sha256 = "190n1n4k0xbycz25bn0d2gnfxd8w6scz3nlixl7w2k2jvpqlcs3n";
+
   };
 
-  why2 = fetchurl {
-    url    = "http://why.lri.fr/download/why-2.40.tar.gz";
-    sha256 = "0h1mbpxsgwvf3pbl0qbg22j6f4v1ffka24ap1ajbjk9b1yb3ali8";
-  };
+  preConfigure = lib.optionalString stdenv.cc.isClang "configureFlagsArray=(\"--with-cpp=clang -E -C\")";
 
   nativeBuildInputs = [ autoconf makeWrapper ];
 
   buildInputs = with ocamlPackages; [
-    ncurses ocaml findlib ltl2ba ocamlgraph
-    lablgtk coq graphviz zarith why3 apron
+    ncurses ocaml findlib ltl2ba ocamlgraph yojson menhir camlzip
+    lablgtk coq graphviz zarith apron why3 mlgmpidl doxygen
   ];
 
+  enableParallelBuilding = true;
 
-  # Experimentally, the build segfaults with high core counts
-  enableParallelBuilding = false;
-
-  unpackPhase = ''
-    tar xf $src
-    tar xf $why2
-  '';
-
-  buildPhase = ''
-    cd frama*
-    ./configure --prefix=$out
-    # It is not parallel safe
-    make
-    make install
-    cd ../why*
-    FRAMAC=$out/bin/frama-c ./configure --prefix=$out
-    make
-    make install
+  fixupPhase = ''
     for p in $out/bin/frama-c{,-gui};
     do
       wrapProgram $p --prefix OCAMLPATH ':' ${ocamlpath}
     done
   '';
 
-  # Enter frama-c directory before patching
-  prePatch = ''cd frama*'';
-  patches = [ ./dynamic.diff ];
-  postPatch = ''
-    # strip absolute paths to /usr/bin
-    for file in ./configure ./share/Makefile.common ./src/*/configure; do #*/
-      substituteInPlace $file  --replace '/usr/bin/' ""
-    done
+  # Allow loading of external Frama-C plugins
+  setupHook = writeText "setupHook.sh" ''
+    addFramaCPath () {
+      if test -d "''$1/lib/frama-c/plugins"; then
+        export FRAMAC_PLUGIN="''${FRAMAC_PLUGIN}''${FRAMAC_PLUGIN:+:}''$1/lib/frama-c/plugins"
+        export OCAMLPATH="''${OCAMLPATH}''${OCAMLPATH:+:}''$1/lib/frama-c/plugins"
+      fi
 
-    substituteInPlace ./src/plugins/aorai/aorai_register.ml --replace '"ltl2ba' '"${ltl2ba}/bin/ltl2ba'
+      if test -d "''$1/lib/frama-c"; then
+        export OCAMLPATH="''${OCAMLPATH}''${OCAMLPATH:+:}''$1/lib/frama-c"
+      fi
 
-    cd ../why*
+      if test -d "''$1/share/frama-c/"; then
+        export FRAMAC_EXTRA_SHARE="''${FRAMAC_EXTRA_SHARE}''${FRAMAC_EXTRA_SHARE:+:}''$1/share/frama-c"
+      fi
 
-    substituteInPlace ./Makefile.in --replace '-warn-error A' '-warn-error A-3'    
-    substituteInPlace ./frama-c-plugin/Makefile --replace 'shell frama-c' "shell $out/bin/frama-c"
-    substituteInPlace ./jc/jc_make.ml --replace ' why-dp '       " $out/bin/why-dp "
-    substituteInPlace ./jc/jc_make.ml --replace "?= why@\n"      "?= $out/bin/why@\n"
-    substituteInPlace ./jc/jc_make.ml --replace ' gwhy-bin@'     " $out/bin/gwhy-bin@"
-    substituteInPlace ./jc/jc_make.ml --replace ' why3 '         " ${why3}/bin/why3 "
-    substituteInPlace ./jc/jc_make.ml --replace ' why3ide '      " ${why3}/bin/why3ide "
-    substituteInPlace ./jc/jc_make.ml --replace ' why3replayer ' " ${why3}/bin/why3replayer "
-    substituteInPlace ./jc/jc_make.ml --replace ' why3ml '       " ${why3}/bin/why3ml "
-    substituteInPlace ./jc/jc_make.ml --replace ' coqdep@'       " ${coq}/bin/coqdep@"
-    substituteInPlace ./jc/jc_make.ml --replace 'coqc'           " ${coq}/bin/coqc"
-    substituteInPlace ./frama-c-plugin/register.ml --replace ' jessie ' " $out/bin/jessie "
-    cd ..
+    }
+
+    addEnvHooks "$targetOffset" addFramaCPath
   '';
 
+
   meta = {
     description = "An extensible and collaborative platform dedicated to source-code analysis of C software";
     homepage    = http://frama-c.com/;
diff --git a/pkgs/development/tools/analysis/frama-c/dynamic.diff b/pkgs/development/tools/analysis/frama-c/dynamic.diff
deleted file mode 100644
index 737cad0cda4..00000000000
--- a/pkgs/development/tools/analysis/frama-c/dynamic.diff
+++ /dev/null
@@ -1,12 +0,0 @@
---- a/src/kernel_services/plugin_entry_points/dynamic.ml	2016-05-30 16:15:22.000000000 +0200
-+++ b/src/kernel_services/plugin_entry_points/dynamic.ml	2016-10-13 18:25:31.000000000 +0200
-@@ -270,7 +270,8 @@
-   load_path :=
-     List.fold_right (add_dir ~user:true) path
-       (List.fold_right (add_dir ~user:false) Config.plugin_dir []);
--  let findlib_path = String.concat ":" !load_path in
-+  let findlib_path = String.concat ":" (!load_path @
-+    try [Sys.getenv "OCAMLPATH"] with Not_found -> []) in
-   Klog.debug ~dkey "setting findlib path to %s" findlib_path;
-   Findlib.init ~env_ocamlpath:findlib_path ()
- 
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 8b082ccf7c9..f9235c30ffb 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -23079,7 +23079,7 @@ in
 
   veriT = callPackage ../applications/science/logic/verit {};
 
-  why3 = callPackage ../applications/science/logic/why3 {};
+  why3 = callPackage ../applications/science/logic/why3 { };
 
   workcraft = callPackage ../applications/science/logic/workcraft {};