diff --git a/pkgs/development/coq-modules/validsdp/default.nix b/pkgs/development/coq-modules/validsdp/default.nix
new file mode 100644
index 000000000000..b4ba02a076bc
--- /dev/null
+++ b/pkgs/development/coq-modules/validsdp/default.nix
@@ -0,0 +1,120 @@
+{
+  coq,
+  mkCoqDerivation,
+  mathcomp,
+  bignums,
+  flocq,
+  coquelicot,
+  interval,
+  mathcomp-reals-stdlib,
+  multinomials,
+  coqeal,
+  lib,
+  version ? null,
+}:
+
+let
+  repo = "validsdp";
+  owner = "validsdp";
+
+  inherit version;
+  defaultVersion =
+    let
+      case = coq: mc: out: {
+        cases = [
+          coq
+          mc
+        ];
+        inherit out;
+      };
+    in
+    with lib.versions;
+    lib.switch
+      [ coq.coq-version mathcomp.version ]
+      [
+        (case (range "9.0" "9.1") (isGe "2.3.0") "1.1.0")
+      ]
+      null;
+  release = {
+    "1.1.0".sha256 = "sha256-lbESAFBEBpOShNFh6RZQYPLRhdqYvdKBrxJOMy2L+Ws=";
+  };
+  releaseRev = v: "v${v}";
+
+  # list of packages sorted by dependency order
+  packages = {
+    "libvalidsdp" = [ ];
+    "validsdp" = [ "libvalidsdp" ];
+  };
+
+  validsdp_ =
+    package:
+    let
+      libvalidsdp-deps = [
+        mathcomp.field
+        bignums
+        flocq
+        coquelicot
+        interval
+        mathcomp-reals-stdlib
+      ];
+      validsdp-deps = [
+        mathcomp.field
+        bignums
+        flocq
+        interval
+        mathcomp-reals-stdlib
+        multinomials
+        coqeal
+        coq.ocamlPackages.osdp
+        coq.ocamlPackages.ocplib-simplex
+      ];
+      intra-deps = map validsdp_ packages.${package};
+      pkgpath = lib.switch package [
+        {
+          case = "libvalidsdp";
+          out = "libvalidsdp";
+        }
+        {
+          case = "validsdp";
+          out = ".";
+        }
+      ] package;
+      pname = package;
+
+      derivation = mkCoqDerivation ({
+        inherit
+          version
+          pname
+          defaultVersion
+          release
+          releaseRev
+          repo
+          owner
+          ;
+
+        namePrefix = [
+          "coq"
+        ];
+
+        mlPlugin = package == "validsdp";
+
+        propagatedBuildInputs =
+          intra-deps
+          ++ lib.optionals (package == "libvalidsdp") libvalidsdp-deps
+          ++ lib.optionals (package == "validsdp") validsdp-deps;
+
+        preBuild = ''
+          cd ${pkgpath}
+        '';
+
+        meta = {
+          description = "ValidSDP";
+          license = lib.licenses.lgpl21Plus;
+        };
+
+        passthru = lib.mapAttrs (package: deps: validsdp_ package) packages;
+      });
+    in
+    derivation;
+in
+validsdp_ "validsdp"
diff --git a/pkgs/development/ocaml-modules/osdp/default.nix b/pkgs/development/ocaml-modules/osdp/default.nix
new file mode 100644
index 000000000000..05af890d045a
--- /dev/null
+++ b/pkgs/development/ocaml-modules/osdp/default.nix
@@ -0,0 +1,46 @@
+{
+  lib,
+  buildDunePackage,
+  fetchurl,
+  ocaml,
+  findlib,
+  zarith,
+  ocplib-simplex,
+  csdp,
+  autoconf,
+}:
+
+lib.throwIf (lib.versionAtLeast ocaml.version "5.0")
+  "osdp is not available for OCaml ${ocaml.version}"
+
+  buildDunePackage
+  {
+    pname = "osdp";
+    version = "1.1.1";
+
+    src = fetchurl {
+      url = "https://github.com/Embedded-SW-VnV/osdp/releases/download/v1.1.1/osdp-1.1.1.tgz";
+      hash = "sha256-X7CS2g+MyQPDjhUCvFS/DoqcCXTEw8SCsSGED64TGKQ=";
+    };
+
+    preConfigure = ''
+      autoconf
+    '';
+
+    nativeBuildInputs = [
+      autoconf
+      findlib
+      csdp
+    ];
+    propagatedBuildInputs = [
+      zarith
+      ocplib-simplex
+      csdp
+    ];
+
+    meta = {
+      description = "OCaml Interface to SDP solvers";
+      homepage = "https://github.com/Embedded-SW-VnV/osdp";
+      license = lib.licenses.lgpl3Plus;
+    };
+  }
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index b219b9aba156..530cba2af8f0 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -128,6 +128,7 @@ let
       json = callPackage ../development/coq-modules/json { };
       lemma-overloading = callPackage ../development/coq-modules/lemma-overloading { };
       LibHyps = callPackage ../development/coq-modules/LibHyps { };
+      libvalidsdp = self.validsdp.libvalidsdp;
       ltac2 = callPackage ../development/coq-modules/ltac2 { };
       math-classes = callPackage ../development/coq-modules/math-classes { };
       mathcomp = callPackage ../development/coq-modules/mathcomp { };
@@ -211,6 +212,7 @@ let
       topology = callPackage ../development/coq-modules/topology { };
       trakt = callPackage ../development/coq-modules/trakt { };
       unicoq = callPackage ../development/coq-modules/unicoq { };
+      validsdp = callPackage ../development/coq-modules/validsdp { };
       vcfloat = callPackage ../development/coq-modules/vcfloat (
         lib.optionalAttrs (lib.versions.range "8.16" "8.18" self.coq.version) {
           interval = self.interval.override { version = "4.9.0"; };
diff --git a/pkgs/top-level/ocaml-packages.nix b/pkgs/top-level/ocaml-packages.nix
index 8f73953f7644..8b2548dc0d8c 100644
--- a/pkgs/top-level/ocaml-packages.nix
+++ b/pkgs/top-level/ocaml-packages.nix
@@ -1590,6 +1590,8 @@ let
 
         ordering = callPackage ../development/ocaml-modules/ordering { };
 
+        osdp = callPackage ../development/ocaml-modules/osdp { };
+
         oseq = callPackage ../development/ocaml-modules/oseq { };
 
         otfed = callPackage ../development/ocaml-modules/otfed { };