diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 0db5e979dd081002ec632d3938b0b032d9cb04ed..dd9c7d3f3b5c1c1f63367e9f776bd0360f0e8689 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -162,7 +162,9 @@ validate:
   needs: ["compile"]
   dependencies:
     - compile
-  script: make validate
+  script:
+    - make validate 2>&1 | tee validation-results.txt
+    - scripts/check-validation-output.sh validation-results.txt
 
 validate-classic:
   extends:
diff --git a/scripts/check-validation-output.sh b/scripts/check-validation-output.sh
new file mode 100755
index 0000000000000000000000000000000000000000..ea9df03201802df81e18f17ff6b205909c594848
--- /dev/null
+++ b/scripts/check-validation-output.sh
@@ -0,0 +1,66 @@
+#!/bin/sh
+set -e
+
+RESULTS="$1"
+
+[ -e "$RESULTS" ] || exit 2
+
+OBSERVED="/tmp/observed-validation-output"
+EXPECTED="/tmp/expected-validation-output"
+
+# strip the list of files and COQDEP output
+grep -v 'COQDEP VFILES' "$RESULTS" | grep -v '"coqchk" -silent' > "$OBSERVED"
+
+cat > $EXPECTED <<EOF
+
+CONTEXT SUMMARY
+===============
+
+* Theory: Set is predicative
+  
+* Axioms: <none>
+  
+* Constants/Inductives relying on type-in-type: <none>
+  
+* Constants/Inductives relying on unsafe (co)fixpoints: <none>
+  
+* Inductives whose positivity is assumed: <none>
+  
+EOF
+
+if ! diff --brief "$OBSERVED" "$EXPECTED" > /dev/null
+then
+    echo "[!!] Validation output does not match expected output."
+    echo "[II] Trying workaround for https://github.com/coq/coq/issues/13324"
+
+    # strip the list of files, COQDEP output, and 
+    # filter bogus ltac: axioms (see Coq issue 13324)
+    grep -v 'COQDEP VFILES' "$RESULTS" | grep -v '"coqchk" -silent' | grep -v "ltac_gen_subproof" > "$OBSERVED"
+    # the list of axioms should now be an empty list
+    cat > $EXPECTED <<EOF
+
+CONTEXT SUMMARY
+===============
+
+* Theory: Set is predicative
+  
+* Axioms:
+  
+* Constants/Inductives relying on type-in-type: <none>
+  
+* Constants/Inductives relying on unsafe (co)fixpoints: <none>
+  
+* Inductives whose positivity is assumed: <none>
+  
+EOF
+    if ! diff --brief "$OBSERVED" "$EXPECTED" > /dev/null
+    then
+        echo "[!!] Validation output still does not match expected output."
+        diff -u "$OBSERVED" "$EXPECTED"
+        exit 3
+    fi
+fi
+
+# if we get here, we saw the expected output
+echo "[II] Validation succeeded."
+exit 0