diff --git a/pkgs/development/coq-modules/wasmcert/default.nix b/pkgs/development/coq-modules/wasmcert/default.nix
new file mode 100644
index 000000000000..cf9e8a49f7ba
--- /dev/null
+++ b/pkgs/development/coq-modules/wasmcert/default.nix
@@ -0,0 +1,67 @@
+{
+  lib,
+  mkCoqDerivation,
+  callPackage,
+  coq,
+  flocq,
+  parseque,
+  mathcomp-boot,
+  compcert,
+  ExtLib,
+  version ? null,
+}:
+
+with lib;
+mkCoqDerivation {
+  pname = "wasm";
+  repo = "WasmCert-Coq";
+  owner = "WasmCert";
+
+  inherit version;
+  defaultVersion =
+    let
+      case = coq: mc: out: {
+        cases = [
+          coq
+          mc
+        ];
+        inherit out;
+      };
+    in
+    with lib.versions;
+    lib.switch
+      [ coq.coq-version mathcomp-boot.version ]
+      [
+        (case (isEq "8.20") (isEq "2.4") "2.1.0")
+      ]
+      null;
+
+  release."2.1.0".sha256 = "sha256-k094mxDLLeelYP+ABm+dm6Y5YrachrbhNeZhfwLHNRo=";
+
+  mlPlugin = true;
+  useDune = true;
+
+  propagatedBuildInputs = [
+    ExtLib
+    mathcomp-boot
+    parseque
+    flocq
+    compcert
+  ];
+
+  buildInputs = [
+    coq.ocamlPackages.mdx
+    coq.ocamlPackages.linenoise
+    coq.ocamlPackages.wasm
+  ];
+
+  releaseRev = v: "v${v}";
+
+  passthru.tests.HelloWorld = callPackage ./test.nix { };
+
+  meta = {
+    description = "Wasm mechanisation in Coq/Rocq";
+    maintainers = with maintainers; [ womeier ];
+    license = licenses.mit;
+  };
+}
diff --git a/pkgs/development/coq-modules/wasmcert/test.nix b/pkgs/development/coq-modules/wasmcert/test.nix
new file mode 100644
index 000000000000..ba548f794cdd
--- /dev/null
+++ b/pkgs/development/coq-modules/wasmcert/test.nix
@@ -0,0 +1,30 @@
+{
+  stdenv,
+  coq,
+  wasmcert,
+}:
+
+stdenv.mkDerivation {
+  pname = "wasmcert-interpreter-test";
+  inherit (wasmcert) src version;
+  nativeCheckInputs = [
+    wasmcert
+    coq
+  ];
+  dontConfigure = true;
+  dontBuild = true;
+  doCheck = true;
+
+  checkPhase = ''
+    coqc .ci/import_test.v
+
+    wasm_coq_interpreter tests/add.wasm -r main
+
+    if [ $? -ne 0 ]; then
+      echo "Wasm_coq_interpreter failed to run hello world program"
+      exit 1
+    fi
+  '';
+
+  installPhase = "touch $out";
+}
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index 5b14584990a0..f7a41d8a05f4 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -245,6 +245,7 @@ let
           };
         })
       );
+      wasmcert = callPackage ../development/coq-modules/wasmcert { };
       waterproof = callPackage ../development/coq-modules/waterproof { };
       zorns-lemma = callPackage ../development/coq-modules/zorns-lemma { };
       filterPackages = doesFilter: if doesFilter then filterCoqPackages self else self;