diff --git a/pkgs/by-name/al/alt-ergo-free/package.nix b/pkgs/by-name/al/alt-ergo-free/package.nix
new file mode 100644
index 000000000000..0d55721223af
--- /dev/null
+++ b/pkgs/by-name/al/alt-ergo-free/package.nix
@@ -0,0 +1,40 @@
+{
+  fetchurl,
+  lib,
+  ocamlPackages,
+  stdenv,
+}:
+
+ocamlPackages.buildDunePackage (finalAttrs: {
+  pname = "alt-ergo-free";
+  version = "2.4.3";
+
+  src = fetchurl {
+    url = "https://github.com/OCamlPro/alt-ergo/releases/download/v${finalAttrs.version}-free/alt-ergo-${finalAttrs.version}-free.tar.gz";
+    hash = "sha256-ksVP9HH9pY+T6Es/wgC9pGd805AGw1e1vgfVlNGCXG8=";
+  };
+
+  nativeBuildInputs = [ ocamlPackages.menhir ];
+
+  sourceRoot = ".";
+
+  buildInputs = with ocamlPackages; [
+    cmdliner
+    camlzip
+    stdlib-shims
+    dune-configurator
+    dune-build-info
+    num
+    psmt2-frontend
+    ocplib-simplex_0_4
+    zarith
+    seq
+  ];
+
+  meta = {
+    description = "High-performance theorem prover and SMT solver";
+    homepage = "https://alt-ergo.ocamlpro.com/";
+    license = lib.licenses.cecill-c;
+    maintainers = with lib.maintainers; [ redianthus ];
+  };
+})
diff --git a/pkgs/development/ocaml-modules/ocplib-simplex/0_4.nix b/pkgs/development/ocaml-modules/ocplib-simplex/0_4.nix
new file mode 100644
index 000000000000..12bd700b601b
--- /dev/null
+++ b/pkgs/development/ocaml-modules/ocplib-simplex/0_4.nix
@@ -0,0 +1,41 @@
+{
+  lib,
+  fetchFromGitHub,
+  stdenv,
+  autoreconfHook,
+  ocaml,
+  findlib,
+}:
+
+stdenv.mkDerivation (finalAttrs: {
+  pname = "ocplib-simplex";
+  version = "0.4.1";
+
+  src = fetchFromGitHub {
+    owner = "OCamlPro";
+    repo = finalAttrs.pname;
+    rev = "v${finalAttrs.version}";
+    hash = "sha256-bhlTBpJg031x2lUjwuVrhQgOGmDLW/+0naN8wRjv6i4=";
+  };
+
+  nativeBuildInputs = [
+    autoreconfHook
+    ocaml
+    findlib
+  ];
+
+  preInstall = ''
+    mkdir -p $out/lib/ocaml/${ocaml.version}/site-lib/
+  '';
+
+  postInstall = ''
+    mv $out/lib/${finalAttrs.pname} $out/lib/ocaml/${ocaml.version}/site-lib
+  '';
+
+  meta = {
+    description = "OCaml library implementing a simplex algorithm, in a functional style, for solving systems of linear inequalities";
+    homepage = "https://github.com/OCamlPro/ocplib-simplex";
+    license = lib.licenses.lgpl21Only;
+    maintainers = with lib.maintainers; [ redianthus ];
+  };
+})
diff --git a/pkgs/top-level/ocaml-packages.nix b/pkgs/top-level/ocaml-packages.nix
index 711c52f3d305..4552fa7b837d 100644
--- a/pkgs/top-level/ocaml-packages.nix
+++ b/pkgs/top-level/ocaml-packages.nix
@@ -1563,6 +1563,8 @@ let
 
         ocplib-simplex = callPackage ../development/ocaml-modules/ocplib-simplex { };
 
+        ocplib-simplex_0_4 = callPackage ../development/ocaml-modules/ocplib-simplex/0_4.nix { };
+
         ocsigen-ppx-rpc = callPackage ../development/ocaml-modules/ocsigen-ppx-rpc { };
 
         ocsigen_server = callPackage ../development/ocaml-modules/ocsigen-server { };