diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index a1c2f0ea..8e1d090b 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -33,6 +33,7 @@ jobs:
     - name: Update OPAM & EasyCrypt dependencies
       run: |
         opam update
+        opam pin alt-ergo 2.5.2
         opam pin add -n easycrypt easycrypt
         opam install --deps-only easycrypt
     - name: Compile & Install EasyCrypt
diff --git a/config/alt-ergo.nix b/config/alt-ergo.nix
deleted file mode 100644
index 9cc57ca0..00000000
--- a/config/alt-ergo.nix
+++ /dev/null
@@ -1,78 +0,0 @@
-{ 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/easycrypt.project b/easycrypt.project
index 842092c4..f49b5e2f 100644
--- a/easycrypt.project
+++ b/easycrypt.project
@@ -1,7 +1,7 @@
 [general]
 timeout = 30
 
-provers = Alt-Ergo@2.4
+provers = Alt-Ergo@2.5
 provers = CVC4@1.8
 provers = Z3@4.8
 
diff --git a/shell.nix b/shell.nix
index 81081568..a8b1fd32 100644
--- a/shell.nix
+++ b/shell.nix
@@ -1,7 +1,7 @@
 { pkgs ?
     import (fetchTarball {
-      url = https://github.com/NixOS/nixpkgs/archive/53fbe41cf76b6a685004194e38e889bc8857e8c2.tar.gz;
-      sha256 = "sha256:1fyc4kbhv7rrfzya74yprvd70prlcsv56b7n0fv47kn7rznvvr2b";
+      url = https://github.com/NixOS/nixpkgs/archive/51063ed4f2343a59fdeebb279bb81d87d453942b.tar.gz;
+      sha256 = "sha256:0my8bdc7js7gdcl8z8ik49sl9gccqz39xg8q335sharf5qxq13ww";
     }) {}
 , full ? true
 }:
@@ -30,7 +30,7 @@ let
     ocamlPackages = oc;
     why3 = why;
   };
-  altergo = callPackage ./config/alt-ergo.nix { ocamlPackages = oc; } ;
+  altergo = alt-ergo.override { ocamlPackages = oc; } ;
 in
 
 mkShell ({