diff --git a/config/alt-ergo.nix b/config/alt-ergo.nix
new file mode 100644
index 00000000..9cc57ca0
--- /dev/null
+++ b/config/alt-ergo.nix
@@ -0,0 +1,78 @@
+{ stdenv, autoreconfHook, fetchFromGitHub, fetchpatch, lib, which, ocamlPackages }:
+
+let ocplib-simplex =
+
+  let
+    inherit (ocamlPackages) ocaml findlib;
+    pname = "ocplib-simplex";
+    version = "0.4";
+  in
+
+  stdenv.mkDerivation {
+    name = "ocaml${ocaml.version}-${pname}-${version}";
+
+    src = fetchFromGitHub {
+      owner = "OCamlPro-Iguernlala";
+      repo = pname;
+      rev = "v${version}";
+      sha256 = "09niyidrjzrj8g1qwx4wgsdf5m6cwrnzg7zsgala36jliic4di60";
+    };
+
+    nativeBuildInputs = [ autoreconfHook ocaml findlib ];
+
+    strictDeps = true;
+
+    installFlags = [ "LIBDIR=$(OCAMLFIND_DESTDIR)" ];
+
+    createFindlibDestdir = true;
+
+  };
+in
+
+let
+  pname = "alt-ergo";
+  version = "2.4.3";
+
+  configureScript = "ocaml unix.cma configure.ml";
+
+  src = fetchFromGitHub {
+    owner = "OCamlPro";
+    repo = pname;
+    rev = "refs/tags/${version}";
+    hash = "sha256-2XARGr8rLiPMOM0rBBoRv5tZvKYtkLkJctGqLYkMe7Q=";
+  };
+in
+
+let alt-ergo-lib = ocamlPackages.buildDunePackage rec {
+  pname = "alt-ergo-lib";
+  inherit version src configureScript;
+  configureFlags = [ pname ];
+  nativeBuildInputs = [ which ];
+  buildInputs = with ocamlPackages; [ dune-configurator ];
+  propagatedBuildInputs = with ocamlPackages; [ dune-build-info num ocplib-simplex seq stdlib-shims zarith ];
+}; in
+
+let alt-ergo-parsers = ocamlPackages.buildDunePackage rec {
+  pname = "alt-ergo-parsers";
+  inherit version src configureScript;
+  configureFlags = [ pname ];
+  nativeBuildInputs = [ which ocamlPackages.menhir ];
+  propagatedBuildInputs = [ alt-ergo-lib ] ++ (with ocamlPackages; [ camlzip psmt2-frontend ]);
+}; in
+
+ocamlPackages.buildDunePackage {
+
+  inherit pname version src configureScript;
+
+  configureFlags = [ pname ];
+
+  nativeBuildInputs = [ which ocamlPackages.menhir ];
+  buildInputs = [ alt-ergo-parsers ocamlPackages.cmdliner ];
+
+  meta = {
+    description = "High-performance theorem prover and SMT solver";
+    homepage    = "https://alt-ergo.ocamlpro.com/";
+    license     = lib.licenses.ocamlpro_nc;
+    maintainers = [ lib.maintainers.thoughtpolice ];
+  };
+}
diff --git a/shell.nix b/shell.nix
new file mode 100644
index 00000000..611ca747
--- /dev/null
+++ b/shell.nix
@@ -0,0 +1,41 @@
+with import (fetchTarball {
+    url = https://github.com/NixOS/nixpkgs/archive/53fbe41cf76b6a685004194e38e889bc8857e8c2.tar.gz;
+    sha256 = "sha256:1fyc4kbhv7rrfzya74yprvd70prlcsv56b7n0fv47kn7rznvvr2b";
+}) {};
+
+let
+  oc = ocaml-ng.ocamlPackages_4_14;
+  why = why3.override {
+    ocamlPackages = oc;
+    ideSupport = false;
+    coqPackages = { coq = null; flocq = null; };
+  };
+  ecVersion = "f7992e1fe5a443a9dcbce2941f708ea7bc78f6e0";
+  ec = (easycrypt.overrideAttrs (_: {
+    src = fetchFromGitHub {
+      owner = "EasyCrypt";
+      repo = "easycrypt";
+      rev = ecVersion;
+      hash = "sha256-CdgF2bFzUPNMQoGCOsJaqKp4pDBMqtFZXB0y1Miwm2c=";
+    };
+    postPatch = ''
+      substituteInPlace dune-project --replace '(name easycrypt)' '(name easycrypt)(version ${ecVersion})'
+    '';
+  })).override {
+    ocamlPackages = oc;
+    why3 = why;
+  };
+  altergo = callPackage ./config/alt-ergo.nix { ocamlPackages = oc; } ;
+in
+
+mkShell {
+  packages = [
+    ec
+    altergo
+    cvc4
+    z3
+  ];
+
+  JASMINC = "${jasmin-compiler.bin}/bin/jasminc";
+  EC_RDIRS = "Jasmin:${jasmin-compiler.lib}/lib/jasmin/easycrypt";
+}