diff --git a/pkgs/development/coq-modules/itauto/default.nix b/pkgs/development/coq-modules/itauto/default.nix
index e2dfe98cf989..804fc8ee87e5 100644
--- a/pkgs/development/coq-modules/itauto/default.nix
+++ b/pkgs/development/coq-modules/itauto/default.nix
@@ -1,16 +1,18 @@
-{ lib, mkCoqDerivation, coq, version ? null }:
+{ lib, callPackage, mkCoqDerivation, coq, version ? null }:
 
-mkCoqDerivation rec {
+(mkCoqDerivation rec {
   pname = "itauto";
   owner = "fbesson";
   domain = "gitlab.inria.fr";
 
+  release."8.17.0".sha256 = "sha256-fgdnKchNT1Hyrq14gU8KWYnlSfg3qlsSw5A4+RoA26w=";
   release."8.16.0".sha256 = "sha256-4zAUYGlw/pBcLPv2GroIduIlvbfi1+Vy+TdY8KLCqO4=";
   release."8.15.0".sha256 = "sha256:10qpv4nx1p0wm9sas47yzsg9z22dhvizszfa21yff08a8fr0igya";
   release."8.14.0".sha256 = "sha256:1k6pqhv4dwpkwg81f2rlfg40wh070ks1gy9r0ravm2zhsbxqcfc9";
   release."8.13+no".sha256 = "sha256-gXoxtLcHPoyjJkt7WqvzfCMCQlh6kL2KtCGe3N6RC/A=";
   inherit version;
   defaultVersion = with lib.versions; lib.switch coq.coq-version [
+    { case = isEq "8.17"; out = "8.17.0"; }
     { case = isEq "8.16"; out = "8.16.0"; }
     { case = isEq "8.15"; out = "8.15.0"; }
     { case = isEq "8.14"; out = "8.14.0"; }
@@ -21,9 +23,14 @@ mkCoqDerivation rec {
   nativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]);
   enableParallelBuilding = false;
 
+  passthru.tests.suite = callPackage ./test.nix {};
+
   meta =  with lib; {
     description = "A reflexive SAT solver parameterised by a leaf tactic and Nelson-Oppen support";
     maintainers = with maintainers; [ siraben ];
     license = licenses.gpl3Plus;
   };
-}
+}).overrideAttrs (o: lib.optionalAttrs
+  (o.version == "dev" || lib.versionAtLeast o.version "8.16") {
+    propagatedBuildInputs = [ coq.ocamlPackages.findlib ];
+})
diff --git a/pkgs/development/coq-modules/itauto/test.nix b/pkgs/development/coq-modules/itauto/test.nix
new file mode 100644
index 000000000000..ef3a85954e61
--- /dev/null
+++ b/pkgs/development/coq-modules/itauto/test.nix
@@ -0,0 +1,27 @@
+{ stdenv, lib, coq, itauto }:
+
+let excluded =
+  lib.optionals (lib.versions.isEq "8.16" itauto.version) [ "arith.v" "refl_bool.v" ]
+; in
+
+stdenv.mkDerivation {
+  pname = "coq${coq.coq-version}-itauto-test";
+  inherit (itauto) src version;
+
+  nativeCheckInputs = [ coq itauto ];
+
+  dontConfigure = true;
+  dontBuild = true;
+  doCheck = true;
+
+  checkPhase = ''
+    cd test-suite
+    for m in *.v
+    do
+      echo -n ${lib.concatStringsSep " " excluded} | grep --silent $m && continue
+      echo $m && coqc $m
+    done
+  '';
+
+  installPhase = "touch $out";
+}