diff --git a/pkgs/development/ocaml-modules/lambdapi/default.nix b/pkgs/development/ocaml-modules/lambdapi/default.nix
new file mode 100644
index 000000000000..5827c5d4b7a5
--- /dev/null
+++ b/pkgs/development/ocaml-modules/lambdapi/default.nix
@@ -0,0 +1,46 @@
+{ lib
+, fetchFromGitHub
+, buildDunePackage
+, alcotest
+, dedukti
+, bindlib
+, camlp-streams
+, cmdliner_1_1
+, menhir
+, pratter
+, sedlex
+, stdlib-shims
+, timed
+, why3
+, yojson
+}:
+
+buildDunePackage rec {
+  pname = "lambdapi";
+  version = "2.2.1";
+
+  minimalOCamlVersion = "4.08";
+
+  src = fetchFromGitHub {
+    owner = "Deducteam";
+    repo = pname;
+    rev = version;
+    hash = "sha256-p2ZjSfiZwkf8X4fSNJx7bAVpTFl4UBHIEANIWF7NGCs=";
+  };
+
+  nativeBuildInputs = [ menhir ];
+  propagatedBuildInputs = [
+    bindlib camlp-streams cmdliner_1_1 pratter sedlex stdlib-shims timed why3 yojson
+  ];
+
+  checkInputs = [ alcotest dedukti ];
+  doCheck = false;  # "Error: Unbound module Cmd"
+
+  meta = with lib; {
+    homepage = "https://github.com/Deducteam/lambdapi";
+    description = "Proof assistant based on the λΠ-calculus modulo rewriting";
+    license = licenses.cecill21;
+    changelog = "https://github.com/Deducteam/lambdapi/raw/${version}/CHANGES.md";
+    maintainers = with maintainers; [ bcdarwin ];
+  };
+}
diff --git a/pkgs/top-level/ocaml-packages.nix b/pkgs/top-level/ocaml-packages.nix
index 86154e879343..a8b5742aaeb7 100644
--- a/pkgs/top-level/ocaml-packages.nix
+++ b/pkgs/top-level/ocaml-packages.nix
@@ -702,6 +702,8 @@ let
 
     ladspa = callPackage ../development/ocaml-modules/ladspa { };
 
+    lambdapi = callPackage ../development/ocaml-modules/lambdapi { };
+
     lambdasoup = callPackage ../development/ocaml-modules/lambdasoup { };
 
     lambda-term = callPackage ../development/ocaml-modules/lambda-term { };