diff --git a/pkgs/development/ocaml-modules/msat/default.nix b/pkgs/development/ocaml-modules/msat/default.nix
new file mode 100644
index 000000000000..d5893dc55e04
--- /dev/null
+++ b/pkgs/development/ocaml-modules/msat/default.nix
@@ -0,0 +1,36 @@
+{ lib, fetchFromGitHub, buildDunePackage
+, iter
+, containers
+, mdx
+}:
+
+buildDunePackage rec {
+  pname = "msat";
+  version = "0.9.1";
+
+  src = fetchFromGitHub {
+    owner = "Gbury";
+    repo = "mSAT";
+    rev = "v${version}";
+    hash = "sha256-ER7ZUejW+Zy3l2HIoFDYbR8iaKMvLZWaeWrOAAYXjG4=";
+  };
+
+  propagatedBuildInputs = [
+    iter
+  ];
+
+  postPatch = ''
+    substituteInPlace dune --replace mdx ocaml-mdx
+  '';
+
+  doCheck = true;
+  checkInputs = [ containers ];
+  nativeCheckInputs = [ mdx.bin ];
+
+  meta = {
+    description = "A modular sat/smt solver with proof output.";
+    homepage = "https://gbury.github.io/mSAT/";
+    license = lib.licenses.asl20;
+    maintainers = [ lib.maintainers.vbgl ];
+  };
+}
diff --git a/pkgs/top-level/ocaml-packages.nix b/pkgs/top-level/ocaml-packages.nix
index 317ecf9f3eeb..b31932759c85 100644
--- a/pkgs/top-level/ocaml-packages.nix
+++ b/pkgs/top-level/ocaml-packages.nix
@@ -1174,6 +1174,8 @@ let
 
     mrmime = callPackage ../development/ocaml-modules/mrmime { };
 
+    msat = callPackage ../development/ocaml-modules/msat { };
+
     mtime_1 =  callPackage ../development/ocaml-modules/mtime/1_x.nix { };
     mtime =  callPackage ../development/ocaml-modules/mtime { };