diff --git a/pkgs/development/coq-modules/atbr/default.nix b/pkgs/development/coq-modules/atbr/default.nix
new file mode 100644
index 000000000000..e1a77312eefa
--- /dev/null
+++ b/pkgs/development/coq-modules/atbr/default.nix
@@ -0,0 +1,21 @@
+{ lib, mkCoqDerivation, coq, version ? null }:
+
+mkCoqDerivation {
+  pname = "atbr";
+  inherit version;
+  defaultVersion = let inherit (lib.versions) range; in
+    lib.switch coq.coq-version [
+      { case = range "8.20" "8.20"; out = "8.20.0"; }
+    ] null;
+  release = {
+    "8.20.0".sha256  = "sha256-Okhtq6Gnq4HA3tEZJvf8JBnmk3OKdm6hC1qINmoShmo=";
+  };
+  releaseRev = v: "v${v}";
+
+  mlPlugin = true;
+
+  meta = {
+    description = "Coq library and tactic for deciding Kleene algebras";
+    license = lib.licenses.lgpl3Plus;
+  };
+}
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index f52c1e5f21d8..47d3c815ccef 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -19,6 +19,7 @@ let
 
       aac-tactics = callPackage ../development/coq-modules/aac-tactics {};
       addition-chains = callPackage ../development/coq-modules/addition-chains {};
+      atbr = callPackage ../development/coq-modules/atbr {};
       autosubst = callPackage ../development/coq-modules/autosubst {};
       bignums = if lib.versionAtLeast coq.coq-version "8.6"
         then callPackage ../development/coq-modules/bignums {}