diff --git a/CHANGES b/CHANGES
index b8d846b91..f0dbcf664 100644
--- a/CHANGES
+++ b/CHANGES
@@ -14,6 +14,9 @@ the Git ChangeLog, the GitHub repo https://github.com/ProofGeneral/PG
     Proof-tree visualization is currently only supported for Coq. The
     prooftree support has been substantially rewritten, making use of
     the much better support since Coq version 8.11.
+*** New command `proof-check-proofs' to generates the proof status
+    of all opaque proofs. Currently only available for Coq, see Coq
+    changes below for more details.
 
 ** Coq changes
 *** support Coq 8.19
@@ -23,15 +26,21 @@ the Git ChangeLog, the GitHub repo https://github.com/ProofGeneral/PG
      modules as coqdep error.
 *** Renew support for proof-tree visualization, see description in
     generic changes above.
-
-
-**** New options coq-compile-extra-coqc-arguments and
-     coq-compile-extra-coqdep-arguments to configure additional
-     command line arguments to calls of, respetively, coqc and coqdep
-     during auto compilation.
-
-**** Fix issues #687 and #688 where the omit-proofs feature causes
-     errors on correct code.
+*** New command `proof-check-proofs' to generates the proof status
+    of all opaque proofs. This command is useful for a development
+    process where invalid proofs are permitted and vos compilation and
+    the omit proofs feature are used to work at the most interesting
+    or challenging point instead of on the first invalid proof. The
+    command generates a list of all opaque proofs in the current
+    buffer together with the information whether the proof script is
+    currently valid or invalid. The command can also be run in batch
+    mode, for instance in a continuous integration environment.
+*** New options coq-compile-extra-coqc-arguments and
+    coq-compile-extra-coqdep-arguments to configure additional
+    command line arguments to calls of, respetively, coqc and coqdep
+    during auto compilation.
+*** Fix issues #687 and #688 where the omit-proofs feature causes
+    errors on correct code.
 
 
 * Changes of Proof General 4.5 from Proof General 4.4
diff --git a/ci/simple-tests/Makefile b/ci/simple-tests/Makefile
index 786ce6067..70b15a1fd 100644
--- a/ci/simple-tests/Makefile
+++ b/ci/simple-tests/Makefile
@@ -15,7 +15,7 @@ COQ_SUCCESS:=$(COQ_TESTS:.el=.success)
 QRHL_SUCCESS:=$(QRHL_TESTS:.el=.success)
 
 .PHONY: coq-all
-coq-all: $(COQ_SUCCESS)
+coq-all: $(COQ_SUCCESS) coq-proof-stat-batch-test
 
 .PHONY: qrhl-all
 qrhl-all: $(QRHL_SUCCESS)
@@ -25,6 +25,20 @@ qrhl-all: $(QRHL_SUCCESS)
 		-f ert-run-tests-batch-and-exit \
 	&& touch $@
 
+# The following tests the batch mode functionality of
+# proof-check-proofs. It generates human readable and TAP output for
+# proof_stat.v and compares it with the expected output in file
+# proof_stat.exp-out.
+coq-proof-stat-batch-test:
+	rm -rf proof_stat.gen-out
+	emacs -batch -l ../../generic/proof-site.el proof_stat.v \
+	      --eval '(proof-check-proofs nil "proof_stat.gen-out")'
+	emacs -batch -l ../../generic/proof-site.el proof_stat.v \
+	      --eval '(proof-check-proofs t "proof_stat.gen-out")'
+	cmp proof_stat.gen-out proof_stat.exp-out && \
+		touch coq-proof-stat-batch-test
+
 .PHONY: clean
 clean:
 	rm -f *.vo *.glob *.vio *.vos *.vok .*.aux *.success
+	rm -f coq-proof-stat-batch-test proof_stat.gen-out
diff --git a/ci/simple-tests/README.md b/ci/simple-tests/README.md
index 523975c6e..553448f9b 100644
--- a/ci/simple-tests/README.md
+++ b/ci/simple-tests/README.md
@@ -15,9 +15,15 @@ coq-test-prelude-correct
 coq-test-goals-present
 : test that Proof General shows goals correctly in various
   situations
-coq-test-three-window.el
+coq-test-three-window
 : Test three-pane mode for different frame sizes, including ones that
   are too small for three windows.
+coq-test-proof-stat
+: test proof-check-proofs
+coq-proof-stat-batch-test
+: Batch mode test for proof-check-proofs. There is no Emacs lisp file
+  for this test. It is programmed out in the Makefile goal
+  coq-proof-stat-batch-test.
 
 # Overview of existing tests for qRHL
 
diff --git a/ci/simple-tests/coq-test-omit-proofs.el b/ci/simple-tests/coq-test-omit-proofs.el
index f2c140bc3..ed7aea8d5 100644
--- a/ci/simple-tests/coq-test-omit-proofs.el
+++ b/ci/simple-tests/coq-test-omit-proofs.el
@@ -95,7 +95,8 @@ In particular, test that with proof-omit-proofs-option configured:
 - in this case the proof has normal locked color
 - without prefix arg, the proof is omitted
 - the proof has omitted color then
-- stuff before the proof still has normal color "
+- stuff before the proof still has normal color
+- trailing incomplete proofs are not omitted"
   (message "omit-proofs-omit-and-not-omit: Check several omit proofs features")
   (setq proof-omit-proofs-option t
         proof-three-window-enable nil)
@@ -187,6 +188,23 @@ In particular, test that with proof-omit-proofs-option configured:
   (should (search-backward "automatic test marker 1" nil t))
   (should (eq (first-overlay-face) 'proof-locked-face))
   (should (search-forward "automatic test marker 2" nil t))
+  (should (eq (first-overlay-face) 'proof-locked-face))
+
+  ;; Check 6: check that a partial proof at the end is not omitted
+  (message "6: check that a partial proof at the end is not omitted")
+  (goto-char (point-min))
+  (proof-goto-point)
+  (wait-for-coq)
+  (should (search-forward "automatic test marker 3" nil t))
+  (forward-line 2)
+  (proof-goto-point)
+  (wait-for-coq)
+  ;; there are 2 goals
+  (with-current-buffer "*goals*"
+    (goto-char (point-min))
+    (should (looking-at "2 \\(?:sub\\)?goals")))
+  ;; the line before should be locked
+  (forward-line -1)
   (should (eq (first-overlay-face) 'proof-locked-face)))
 
 (ert-deftest omit-proofs-never-omit-hints ()
diff --git a/ci/simple-tests/coq-test-proof-stat.el b/ci/simple-tests/coq-test-proof-stat.el
new file mode 100644
index 000000000..821077da8
--- /dev/null
+++ b/ci/simple-tests/coq-test-proof-stat.el
@@ -0,0 +1,84 @@
+;; This file is part of Proof General.
+;; 
+;; © Copyright 2024  Hendrik Tews
+;; 
+;; Authors: Hendrik Tews
+;; Maintainer: Hendrik Tews <hendrik@askra.de>
+;; 
+;; SPDX-License-Identifier: GPL-3.0-or-later
+
+;;; Commentary:
+;;
+;; Test proof-check-proofs.
+
+(defun reset-coq ()
+  "Reset Coq and Proof General.
+Do `proof-shell-exit' to kill Coq and reset the locked region and
+a lot of other internal state of Proof General. Used at the
+beginning of the test when several tests work on the same Coq
+source file."
+  (when (and (boundp 'proof-shell-buffer)
+             (buffer-live-p proof-shell-buffer))
+    (proof-shell-exit t)
+    (message "Coq and Proof General reseted")))
+
+
+(ert-deftest proof-check-correct-stat ()
+  "Test `proof-check-proofs' on a file that is correct in non-opaque parts.
+Test that the report buffer contains the expected output."
+  (setq proof-three-window-enable nil)
+  (reset-coq)
+  (find-file "proof_stat.v")
+
+  ;; run check on file where all errors are in opaque parts
+  (proof-check-proofs nil)
+
+  ;; the result buffer should exist
+  (should (buffer-live-p (get-buffer "*proof-check-report*")))
+  (with-current-buffer "*proof-check-report*"
+    ;; the summary should be correct
+    (goto-char (point-min))
+    (should
+     (search-forward "3 opaque proofs recognized: 1 successful 2 FAILING"
+                     nil t))
+    ;; results for all 3 test lemmas should be correct
+    (mapc
+     (lambda (s) (should (search-forward s nil t)))
+     '("FAIL a1_equal_4"
+       "OK   b_equal_6"
+       "FAIL b2_equal_6"))))
+
+
+(ert-deftest proof-check-error-on-error ()
+  "Test `proof-check-proofs' with errors in non-opaque parts.
+Check that `proof-check-proofs' signals an error with the expected message."
+  (setq proof-three-window-enable nil)
+  (reset-coq)
+  (let (buffer)
+    (unwind-protect
+        (progn
+          (find-file "proof_stat.v")
+          (setq buffer (current-buffer))
+
+          ;; insert an error in non-opaque part
+          (goto-char (point-min))
+          (should (search-forward "automatic test marker 1" nil t))
+          (end-of-line)
+          (insert " X ")
+
+          ;; proof-check-proofs should abort now with an error
+          (condition-case err-desc
+              (progn
+                (proof-check-proofs nil)
+                ;; Still here? Make test fail!
+                (should nil))
+            (error
+             (should
+              (equal (error-message-string err-desc)
+                     "Error encountered outside opaque proofs after line 10")))))
+
+      ;; clean-up modified file in any case
+      (when buffer
+        (with-current-buffer buffer
+          (set-buffer-modified-p nil))
+        (kill-buffer buffer)))))
diff --git a/ci/simple-tests/proof_stat.exp-out b/ci/simple-tests/proof_stat.exp-out
new file mode 100644
index 000000000..9f4f0aa5d
--- /dev/null
+++ b/ci/simple-tests/proof_stat.exp-out
@@ -0,0 +1,16 @@
+Proof check results for proof_stat.v
+
+3 opaque proofs recognized: 1 successful 2 FAILING
+
+  FAIL a1_equal_4
+  OK   b_equal_6
+  FAIL b2_equal_6
+
+
+TAP version 13
+1..3
+not ok 1 - a1_equal_4
+ok 2 - b_equal_6
+not ok 3 - b2_equal_6
+
+
diff --git a/ci/simple-tests/proof_stat.v b/ci/simple-tests/proof_stat.v
new file mode 100644
index 000000000..49411eeeb
--- /dev/null
+++ b/ci/simple-tests/proof_stat.v
@@ -0,0 +1,24 @@
+
+Definition a : nat := 4.
+
+Lemma a1_equal_4 : a = 2 * 2.
+Proof using.
+  simpl.
+  zzzz.                         (* this proof should fail *)
+  trivial.
+Qed.
+
+Definition b : nat :=
+(* automatic test marker 1 *)
+ 6.
+
+Lemma b_equal_6 : b = 2 * 3.
+Proof using.
+  simpl.
+  trivial.
+Qed.
+
+Lemma b2_equal_6 : b = 2 * 3.
+Proof using.                    (* this proof should fail *)
+Qed.
+
diff --git a/coq/coq.el b/coq/coq.el
index a036acde3..b6354bd1f 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1963,6 +1963,12 @@ at `proof-assistant-settings-cmds' evaluation time.")
    proof-script-cmd-prevents-proof-omission #'coq-cmd-prevents-proof-omission
    proof-script-cmd-force-next-proof-kept coq-cmd-force-next-proof-kept)
 
+  ;; proof-check-proofs config
+  (setq
+   proof-get-proof-info-fn #'coq-get-proof-info-fn
+   proof-retract-command-fn #'coq-retract-command)
+
+
   (setq proof-cannot-reopen-processed-files nil)
 
   (proof-config-done)
@@ -2274,6 +2280,25 @@ Function for `proof-tree-display-stop-command'."
     (coq-proof-tree-evar-command "Unset")))
 
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; proof-check-proofs support
+;;
+
+(defun coq-get-proof-info-fn ()
+  "Coq instance of `proof-get-proof-info-fn' for `proof-check-proofs'.
+Return state number followed by the name of the current proof of
+nil in a list."
+  (list
+   coq-last-but-one-statenum
+   (car coq-last-but-one-proofstack)))
+
+(defun coq-retract-command (state)
+  "Coq instance of `proof-retract-command-fn' for `proof-check-proofs'.
+Return command that undos to state."
+  (format "BackTo %d." state))
+   
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; Pre-processing of input string
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index 3e5e72e39..d6adccdbf 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -647,6 +647,7 @@ the behaviour of script management.
 * Configuring undo behaviour::
 * Nested proofs::
 * Omitting proofs for speed::
+* Proof status statistic::
 * Safe (state-preserving) commands::
 * Activate scripting hook::
 * Automatic multiple files::
@@ -1275,6 +1276,58 @@ does only work if the command and the following proof are
 asserted together.
 @end defvar
 
+
+@node Proof status statistic
+@section Proof status statistic
+
+The command @code{proof-check-proofs} builds on the omit-proofs
+feature. Using its machinery, it splits the current buffer into opaque
+proofs and all other material. The other material is asserted in the
+usual way and @code{proof-check-proofs} aborts if it detects an error
+in there. For opaque proofs the command first tries to assert them in
+the usual way too. If this succeeds the proof is considered valid.
+Otherwise the proof is replaced with
+@code{proof-script-proof-admit-command} and the proof is considered
+invalid. To associate theorem names with opaque proofs, the function
+@code{proof-get-proof-info-fn} is called, which is identical to
+@code{proof-tree-get-proof-info}, @xref{Proof Tree Elisp
+configuration}.
+
+To enable proof status statistics, the omit-proofs feature must be
+configured, @xref{Omitting proofs for speed}. Additionally, the
+following settings must be configured.
+
+@c TEXI DOCSTRING MAGIC: proof-get-proof-info-fn
+@defvar proof-get-proof-info-fn 
+Return proof name and state number for @samp{@code{proof-check-proofs}}.@*
+Proof assistant specific function for @samp{@code{proof-check-proofs}}. This
+function takes no arguments, it is called after completely
+processing the proof script up to a certain point (including all
+callbacks in spans). It must return a list, which contains, in
+the following order:
+
+* the current state number (as positive integer)
+* the name of the current proof (as string) or nil
+
+The proof assistant should return to the same state when the
+state number is supplied to @samp{@code{proof-retract-command-fn}}.
+Processing the command returned by @samp{@code{proof-retract-command-fn}}
+without processing any other command after calling this function
+should be a no-op.
+
+(This function has the same signature and specification as
+@samp{@code{proof-tree-get-proof-info}}.)
+@end defvar
+
+@c TEXI DOCSTRING MAGIC: proof-retract-command-fn
+@defvar proof-retract-command-fn 
+Function for retract command to a certain state.@*
+This function takes a state as argument as returned by
+@samp{@code{proof-get-proof-info-fn}}. It should return a command that brings
+the proof assistant back to the same state.
+@end defvar
+
+
 @node Safe (state-preserving) commands
 @section Safe (state-preserving) commands
 
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 3d1eac28d..de74c7c1d 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -1916,6 +1916,7 @@ General covered in this chapter.
 * View of processed files ::    
 * Retracting across files::     
 * Asserting across files::      
+* Proof status statistic::
 * Automatic multiple file handling::
 * Escaping script management::
 * Editing features::
@@ -2256,6 +2257,81 @@ unmodified buffers.  This is particularly useful as assertion may cause
 the proof assistant to automatically process other files.
 
 
+@node Proof status statistic
+@section Proof status statistic
+@cindex Proof status statistic
+
+The command @code{proof-check-proofs} (menu @code{Proof-General ->
+Check Opaque Proofs}) generates the proof status of all opaque proofs
+in the current buffer, i.e., it generates an overview that shows which
+of the opaque proofs in the current buffer are currently valid and
+which are failing. When used interactively, the proof status is shown
+in the buffer @code{*proof-check-report*} (as long as
+@code{proof-check-report-buffer} is not changed).
+
+Currently @code{proof-check-proofs} does only work for Coq.
+
+@c TEXI DOCSTRING MAGIC: proof-check-proofs
+@deffn Command proof-check-proofs tap &optional batch
+Generate an overview about valid and invalid proofs.@*
+This command completely processes the current buffer and
+generates an overview about all the opaque proofs in it and
+whether their proof scripts are valid or invalid.
+
+This command makes sense for a development process where invalid
+proofs are permitted and vos compilation and the omit proofs
+feature (see @samp{@code{proof-omit-proofs-configured}}) are used to work at
+the most interesting or challenging point instead of on the first
+invalid proof.
+
+Argument @var{tap}, which can be set by a prefix argument, controls the
+form of the generated overview. Nil, without prefix, gives an
+human readable overview, otherwise it's test anything
+protocol (@var{tap}). Argument @var{batch} controls where the overview goes
+to. If nil, or in an interactive call, the overview appears in
+@samp{@code{proof-check-report-buffer}}. If @var{batch} is a string, it should be a
+filename and the overview is appended there. Otherwise the
+overview is output via @samp{message} such that it appears on stdout
+when this command runs in batch mode.
+
+In the same way as the omit-proofs feature, this command only
+tolerates errors inside scripts of opaque proofs. Any other error
+is reported to the user without generating an overview. The
+overview only contains those names of theorems whose proofs
+scripts are classified as opaque by the omit-proofs feature. For
+Coq for instance, among others, proof scripts terminated with
+@code{'Defined'} are not opaque and do not appear in the generated
+overview.
+
+Note that this command does not (re-)compile required files.
+Files must be required before running this commands, for instance
+by asserting all require commands beforehand.
+@end deffn
+
+@xref{Quick and inconsistent compilation} for enabling vos compilation
+inside Proof General and see @xref{Omitting proofs for speed} for the
+omit-proofs feature.
+
+The interactive use of this commands is limited because it only works
+on the current buffer. However, this commands can also be run in batch
+mode in a script, for instance in a continuous integration
+environment. To run this command on a file in batch mode, use
+
+@verbatim
+emacs -batch -l <your-pg-dir>/generic/proof-site.el <file> \
+      --eval '(proof-check-proofs <tap> <output>)'
+@end verbatim
+
+where @code{<tap>} should be @code{nil} for human readable output and
+@code{t} for test anything protocol. If @code{<output>} is @code{t}
+the proof status appears in the standard output of the Emacs process.
+Otherwise @code{<output>} should be a filename as string in double
+quotes. Then the proof status is appended to this file. (If
+@code{output} is @code{nil} or omitted, the proof status is only put
+into the @code{*proof-check-report*} buffer, which does not make much
+sense in a batch command as the one above.)
+
+
 @node Automatic multiple file handling
 @section Automatic multiple file handling
 
@@ -4232,6 +4308,7 @@ assistant.  It supports most of the generic features of Proof General.
 * Proof using annotations::
 * Multiple File Support::
 * Omitting proofs for speed::
+* Proof status statistic for Coq::
 * Editing multiple proofs::
 * User-loaded tactics::
 * Indentation tweaking::
@@ -5173,6 +5250,21 @@ non-opaque, even if they have proof-local effect only, such as
 @end itemize
 
 
+@node Proof status statistic for Coq
+@section Proof status statistic for Coq
+
+The command @code{proof-check-proofs} (menu @code{Proof-General ->
+Check Opaque Proofs}) generates the proof status of all opaque proofs
+in the current buffer, i.e., it generates an overview that shows which
+of the opaque proofs in the current buffer are currently valid and
+which are failing. This command is useful for a development process
+where invalid proofs are permitted and vos compilation (@xref{Quick
+and inconsistent compilation}) and the omit proofs feature
+(@xref{Omitting proofs for speed}) are used to work at the most
+interesting or challenging point instead of on the first invalid
+proof. See @xref{Proof status statistic} for more details.
+
+
 @node Editing multiple proofs
 @section Editing multiple proofs
 
diff --git a/generic/pg-user.el b/generic/pg-user.el
index d4115a4ba..05b3c46f8 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -26,6 +26,13 @@
 
 (require 'proof-script)	        ; we build on proof-script
 
+;; For seq-group-by inside `proof-check-report'. This is apparently
+;; not automatically loaded in Emacs 26.3. In a real PG session it is
+;; apparently present, but not if `proof-check-proof' is invoked from
+;; the shell as described in the user manual.
+;; XXX Delete this when support for Emacs 26 is dropped (hopefully in Q4/2025).
+(require 'seq)
+
 (eval-when-compile (require 'cl-lib))   ;cl-decf
 (defvar which-func-modes)               ; Defined by which-func.
 
@@ -597,6 +604,226 @@ last use time, to discourage saving these into the users database."
 
 
 
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; Check validity of proofs
+;;
+
+(defun proof-check-report (proof-results tap batch)
+  "Report `proof-check-proofs' results in PROOF-RESULTS in special buffer.
+Report the results of `proof-check-proofs' in buffer
+`proof-check-report-buffer' in human readable form or, if TAP is
+not nil, in test anything protocol (TAP). If BATCH is not nil,
+report the results via message, such that they appear on stdout
+when Emacs runs in batch mode or, when BATCH is a string, append
+the results to the file denoted by BATCH."
+  (let* ((ok-fail (seq-group-by #'car proof-results))
+         (frmt "  %-4s %s")
+         (frmt-face (propertize frmt 'face 'error))
+         (count 1)
+         (inhibit-read-only t)          ; for the report buffer, below
+         coq-proj-dir src-file)
+
+    ;; determine a relative file name for current buffer
+    (when buffer-file-name
+      (setq coq-proj-dir (locate-dominating-file buffer-file-name
+                                                 coq-project-filename)))
+    (if coq-proj-dir
+        (setq src-file (file-relative-name buffer-file-name coq-proj-dir))
+      (setq src-file (buffer-name)))
+
+    ;; generate header
+    (with-current-buffer (get-buffer-create proof-check-report-buffer)
+      (read-only-mode)
+      (buffer-disable-undo)
+      (erase-buffer)
+      (if tap
+          (insert (format "TAP version 13\n1..%d\n" (length proof-results)))
+        ;; human output
+        (insert
+         (propertize (concat "Proof check results for " src-file) 'face 'bold)
+         "\n\n")
+        (insert
+         (format
+          (propertize "%d opaque proofs recognized: %d successful " 'face 'bold)
+          (length proof-results)
+          (length (cdr (assoc t ok-fail)))))
+        (insert (format (propertize "%d FAILING" 'face 'error 'face 'bold)
+                        (length (cdr (assoc nil ok-fail)))))
+        (insert "\n\n"))
+      (dolist (pr proof-results)
+        (if tap
+            (progn
+              (insert (format "%sok %d - %s\n"
+                              (if (car pr) "" "not ")
+                              count
+                              (cadr pr)))
+              (setq count (1+ count)))
+          ;; human readable
+          (insert (format (if (car pr) frmt frmt-face)
+                          (if (car pr) "OK  " "FAIL")
+                          (cadr pr)))
+          (insert "\n")))
+      (if batch
+          (progn
+            (insert "\n\n")
+            (if (stringp batch)
+                (append-to-file (point-min) (point-max) batch)
+              (message "%s"
+                       (buffer-substring-no-properties
+                        (point-min) (point-max)))))
+        (goto-char (point-min))
+        (display-buffer (current-buffer))))))
+
+(defun proof-check-chunks (chunks)
+  "Worker function for `proof-check-proofs for processing CHUNKS.
+CHUNKS must be the reversed result of `proof-script-omit-filter'
+for a whole buffer. (Only the top-level must be reversed, the
+commands inside the chunks must be as returned by
+`proof-script-omit-filter', that is in reversed order.) CHUNKS
+must not contain any 'nested-proof chunk.
+
+This function processes the content of CHUNK normally by
+asserting them one by one. Any error reported inside a 'no-proof
+chunk is reported as error to the user. 'proof chunks containing
+errors are silently replaced by
+`proof-script-proof-admit-command'. The result is a list of proof
+status results, one for each 'proof chunk in the same order. Each
+proof-status result is a list with first element `t' or `nil',
+depending on whether the proof failed, and the name of the proof
+as reported by `proof-get-proof-info-fn'."
+  (let (proof-results current-proof-state-and-name)
+    (while chunks
+      (let* ((chunk (car chunks))       ; cdr at end
+             (this-mode (car chunk))
+             (next-mode (car-safe (car-safe (cdr chunks))))
+             (vanillas-rev (nth 1 chunk))
+             ;; add 'empty-action-list flag to last item to avoid the
+             ;; call to `proof-shell-empty-action-list-command'
+             (litem (car vanillas-rev))
+             (lspan-end (span-end (car litem)))
+             (nlitem (list (nth 0 litem) (nth 1 litem) (nth 2 litem)
+                           (cons 'empty-action-list (nth 3 litem))))
+             (vanillas-rev-updated (cons nlitem (cdr vanillas-rev)))
+             error)
+        ;; if this is a proof chunk the next must be no-proof or must not exist
+        (cl-assert (or (not (eq this-mode 'proof))
+                       (or (eq next-mode 'no-proof) (eq next-mode nil)))
+                   nil "proof-check: two adjacent proof chunks")
+        (proof-set-queue-endpoints (proof-unprocessed-begin) lspan-end)
+        (proof-add-to-queue (nreverse vanillas-rev-updated) 'advancing)
+        (proof-shell-wait)
+        ;; (redisplay)
+        (unless (eq lspan-end
+                    (and proof-locked-span (span-end proof-locked-span)))
+          ;; not all the spans have been asserted - there was some error
+          (setq error t))
+        (when (and error (eq this-mode 'no-proof))
+          ;; all non-opaque stuff should be error free, abort and tell
+          ;; the user
+          (goto-char (proof-unprocessed-begin))
+          (when (looking-at "$")
+            (forward-line 1))
+          (error "Error encountered outside opaque proofs after line %d"
+                 (line-number-at-pos)))
+            
+        (cond
+         ((and (eq this-mode 'no-proof) (eq next-mode 'proof))
+          ;; non-opaque stuff has been processed error free, next
+          ;; chunk is an opaque proof - record information needed next
+          ;; round
+          (setq current-proof-state-and-name
+                (funcall proof-get-proof-info-fn))
+          (cl-assert (cadr current-proof-state-and-name)
+                     nil "proof-check: no proof name at proof start"))
+
+         ((eq this-mode 'proof)         ; implies next-mode is no-proof
+          ;; opaque proof chunk processed - with or without error
+          (if (not error)
+              (push (list t (cadr current-proof-state-and-name))
+                    proof-results)
+            ;; opaque proof failed, retract, admit, and record error
+            (proof-add-to-queue
+             (list
+              (list nil (list (funcall proof-retract-command-fn
+                                       (car current-proof-state-and-name)))
+                    'proof-done-invisible (list 'invisible))
+              (list nil (list proof-script-proof-admit-command)
+                    'proof-done-invisible (list 'invisible)))
+             'advancing)
+            (proof-shell-wait)
+            (proof-set-locked-end lspan-end)
+            (cl-assert (not (cadr (funcall proof-get-proof-info-fn)))
+                       nil "proof-check: still in proof after admitting")
+            (push (list nil (cadr current-proof-state-and-name))
+                  proof-results))))
+        (setq chunks (cdr chunks))))
+    (nreverse proof-results)))
+    
+(defun proof-check-proofs (tap &optional batch)
+  "Generate an overview about valid and invalid proofs.
+This command completely processes the current buffer and
+generates an overview about all the opaque proofs in it and
+whether their proof scripts are valid or invalid.
+
+This command makes sense for a development process where invalid
+proofs are permitted and vos compilation and the omit proofs
+feature (see `proof-omit-proofs-configured') are used to work at
+the most interesting or challenging point instead of on the first
+invalid proof.
+
+Argument TAP, which can be set by a prefix argument, controls the
+form of the generated overview. Nil, without prefix, gives an
+human readable overview, otherwise it's test anything
+protocol (TAP). Argument BATCH controls where the overview goes
+to. If nil, or in an interactive call, the overview appears in
+`proof-check-report-buffer'. If BATCH is a string, it should be a
+filename and the overview is appended there. Otherwise the
+overview is output via `message' such that it appears on stdout
+when this command runs in batch mode.
+
+In the same way as the omit-proofs feature, this command only
+tolerates errors inside scripts of opaque proofs. Any other error
+is reported to the user without generating an overview. The
+overview only contains those names of theorems whose proofs
+scripts are classified as opaque by the omit-proofs feature. For
+Coq for instance, among others, proof scripts terminated with
+'Defined' are not opaque and do not appear in the generated
+overview.
+
+Note that this command does not (re-)compile required files.
+Files must be required before running this commands, for instance
+by asserting all require commands beforehand."
+  (interactive "P")
+  (unless (and proof-omit-proofs-configured
+               proof-get-proof-info-fn
+               proof-retract-command-fn)
+    (error
+     "proof-check-proofs has not been configured for your proof assistant"))
+  ;; kill proof assistant and retract completely
+  (when (buffer-live-p proof-shell-buffer)
+    (proof-shell-exit t))
+  ;; initialize scripting - taken from `proof-assert-until-point'
+  (proof-activate-scripting nil 'advancing)
+  (let* ((semis (proof-segment-up-to-using-cache (point-max)))
+    	 (vanillas (proof-semis-to-vanillas
+                    semis
+                    '(no-response-display no-goals-display)))
+         (chunks-rev (proof-script-omit-filter vanillas))
+         (last-chunk (car chunks-rev))
+         (chunks (nreverse chunks-rev))
+         proof-results)
+    (when (eq (car last-chunk) 'nested-proof)
+      (error "Nested proof detected at line %d" (nth 2 last-chunk)))
+    (cl-assert (not (eq (caar chunks) 'proof))
+               nil "proof-check: first chunk cannot be a proof")
+    (setq proof-results (proof-check-chunks chunks))
+    (proof-shell-exit t)
+    (proof-check-report proof-results tap batch)))
+
+
+
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 39436918a..d8ede58f9 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -792,6 +792,45 @@ asserted together."
   :group 'proof-script)
 
 
+;; proof-check-proofs configuration
+
+;; The omit-proofs feature must be fully configured for
+;; `proof-check-proofs', see `proof-omit-proofs-configured'.
+
+(defcustom proof-get-proof-info-fn nil
+  "Return proof name and state number for `proof-check-proofs'.
+Proof assistant specific function for `proof-check-proofs'. This
+function takes no arguments, it is called after completely
+processing the proof script up to a certain point (including all
+callbacks in spans). It must return a list, which contains, in
+the following order:
+
+* the current state number (as positive integer)
+* the name of the current proof (as string) or nil
+
+The proof assistant should return to the same state when the
+state number is supplied to `proof-retract-command-fn'.
+Processing the command returned by `proof-retract-command-fn'
+without processing any other command after calling this function
+should be a no-op.
+
+(This function has the same signature and specification as
+`proof-tree-get-proof-info'.)"
+  :type 'function
+  :group 'proof-script)
+
+(defcustom proof-retract-command-fn nil
+  "Function for retract command to a certain state.
+This function takes a state as argument as returned by
+`proof-get-proof-info-fn'. It should return a command that brings
+the proof assistant back to the same state."
+  :type 'function
+  :group 'proof-script)
+
+(defconst proof-check-report-buffer "*proof-check-report*"
+  "Buffer name for the report of `proof-check-proofs'.")
+
+
 ;;
 ;; Proof script indentation
 ;;
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index 77bc05a84..35f6741a9 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -702,7 +702,11 @@ without adjusting window layout."
      :active pg-next-error-regexp]
     ["Scripting Active" proof-toggle-active-scripting
      :style toggle
-     :selected (eq proof-script-buffer (current-buffer))])
+     :selected (eq proof-script-buffer (current-buffer))]
+    ["Check Opaque Proofs" proof-check-proofs
+     :active (and proof-omit-proofs-configured
+               proof-get-proof-info-fn
+               proof-retract-command-fn)])
   "The Proof General generic menu for scripting buffers.")
 
 
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 854bd6bf8..afa2e50b6 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1985,6 +1985,15 @@ Assumes that point is at the end of a command."
 ;; buffer content has been converted to vanilla spans,
 ;; `proof-script-omit-proofs' searches for complete opaque proofs in
 ;; there and replaces them with `proof-script-proof-admit-command'.
+;;
+;; The replacement works in two phases. First,
+;; `proof-script-omit-filter' transfers the list of vanilla spans into
+;; a list of lists of these spans, where each sublist is tagged with
+;; either `'proof' or `'no-proof'. Second, `proof-script-omit-proofs'
+;; replaces the proof parts with admit commands. Partitioning into two
+;; phases makes it possible to reuse the first phase for different
+;; features. See the documentation of `proof-script-omit-filter' for a
+;; specification of the list of lists result type.
 
 (defun proof-move-over-whitespace-to-next-line (pos)
   "Return position of next line if one needs only to jump over white space.
@@ -1999,33 +2008,78 @@ line, otherwise POS."
     (if (eolp)
         (1+ (point))
       pos)))
-  
-(defun proof-script-omit-proofs (vanillas)
-  "Return a copy of VANILLAS with complete opaque proofs omitted.
+
+(defun proof-script-omit-filter (vanillas)
+  "Classify VANILLAS into those which are inside and those outside of proofs.
+Classify the list of vanilla spans VANILLAS into those belonging
+to a proof script that can be omitted by the omit proofs feature
+and those which can not be omitted (either outside proofs or
+inside proofs that cannot be omitted).
+
 See `proof-omit-proofs-configured' for the description of the
 omit proofs feature. This function uses
 `proof-script-proof-start-regexp',
 `proof-script-proof-end-regexp' and
 `proof-script-definition-end-regexp' to search for complete
-opaque proofs in the action list VANILLAS. Complete opaque proofs
-are replaced by `proof-script-proof-admit-command'. The span of
-the admit command contains an 'omitted-proof-region property with
-the region of the omitted proof. This is used in
-`proof-done-advancing-save' to colour the omitted proof with
-`proof-omitted-proof-face'.
-
-Report an error to the (probably surprised) user if another proof
-start is found inside a proof."
+opaque proofs in the action list VANILLAS. Additionally, it uses
+`proof-script-cmd-prevents-proof-omission' and
+`proof-script-cmd-force-next-proof-kept' to detect proofs that
+cannot be omitted.
+
+The result is a list of chunks, where each chunk is a list that
+contains a type tag as first element. The chunk list is returned
+in reversed order, i.e., the first vanilla span in VANILLAS is
+inside the last chunk.
+
+There are three types of chunks: 'proof for commands inside a
+proof that can be omitted, 'no-proof for commands that are
+outside a proof or cannot be omitted, and 'nested for commands
+that contain a nested proof. Note that there may be several
+adjacent 'no-proof chunks, for instance for commands outside a
+proof followed by a proof that cannot be omitted.
+
+The 'proof chunk has 4 elements:
+
+('proof proof-cmds-reversed span-start-first-proof-cmd span-end-first-proof-cmd)
+
+The second, proof-cmds-reversed, contains the vanilla spans from
+VANILLAS corresponding to commands belonging to a proof,
+excluding the first that matched
+`proof-script-proof-start-regexp' and including the last that
+matched `proof-script-proof-end-regexp' in reversed order. The
+third element span-start-first-proof-cmd is the position of the
+start of the command that matched
+`proof-script-proof-start-regexp' and span-end-first-proof-cmd is
+the position of the end of that command.
+
+The 'no-proof chunk has 2 elements.
+
+('no-proof cmds-reversed)
+
+cmds-reversed contains the vanilla spans of VANILLAS in reversed
+order.
+
+The 'nested-proof chunk has 3 elements.
+
+('nested-proof cmds-reversed line-number-nested-proof)
+
+line-number-nested-proof is the line number where the nested
+proof was detected. cmds-reversed is the tail of VANILLAS,
+containing the start of the nested proof, in reversed order. If
+there is a 'nested-proof chunk in the result, it is the first
+chunk."
   (cl-assert
    (and proof-omit-proofs-configured proof-script-proof-start-regexp
         proof-script-proof-end-regexp proof-script-definition-end-regexp
         proof-script-proof-admit-command)
    nil
    "proof-script omit proof feature not properly configured")
-  (let (;; result vanillas with omitted proofs in reverse order
-        result
-        ;; commands of current proof before deciding opaqueness in reverse order
+  (let (;; result in reversed order
+        result-chunks
+        ;; accumulated commands in reversed order before they are put
+        ;; into a result chunk
         maybe-result
+        ;; flag: is the processing loop currently inside a proof or not?
         inside-proof
         proof-start-span-start proof-start-span-end
         ;; t if the proof contains state changing commands and must be kept
@@ -2045,25 +2099,18 @@ start is found inside a proof."
           (progn
             (if (string-match proof-script-proof-start-regexp cmd)
                 ;; Found another proof start inside a proof.
-                ;; Stop omitting and pass the remainder unmodified.
-                ;; The result in `result' is aggregated in reverse
-                ;; order, need to reverse vanillas.
+                ;; Stop classifying and return the remainder as
+                ;; 'no-proof chunk. The commands in `result-chunks'
+                ;; are in reverse order, need to reverse the remaining
+                ;; vanillas.
                 (progn
-                  (setq result (nconc (nreverse vanillas) maybe-result result))
+                  (push (list 'nested-proof
+                              (nconc (nreverse vanillas) maybe-result)
+                              (line-number-at-pos (span-end (car item))))
+                        result-chunks)
                   (setq maybe-result nil)
                   ;; terminate the while loop
-                  (setq vanillas nil)
-                  ;; for Coq nobody will notice the warning, because
-                  ;; the error about nested proofs will pop up shortly
-                  ;; afterwards
-                  (display-warning
-                   '(proof-script)
-                   ;; use the end of the span, because the start is
-                   ;; usually on the preceding  line
-                   (format (concat "found second proof start at line %d"
-                                   " - are there nested proofs?")
-                           (line-number-at-pos (span-end (car item))))))
-
+                  (setq vanillas nil))
               ;; else - no nested proof, but still inside-proof
               (if (and (string-match proof-script-proof-end-regexp cmd)
                        (not proof-must-be-kept))
@@ -2071,43 +2118,13 @@ start is found inside a proof."
                   ;; recognize a state changing command inside the
                   ;; proof that would prohibit throwing the proof
                   ;; away.
-                  (let
-                      ;; Reuse the Qed span for the whole proof,
-                      ;; including the faked Admitted command.
-                      ;; `proof-done-advancing' expects such a span.
-                      ((cmd-span (car item)))
-                    (span-set-property cmd-span 'type 'omitted-proof)
-                    (span-set-property cmd-span
-                                       'cmd proof-script-proof-admit-command)
-                    (span-set-endpoints cmd-span proof-start-span-end
-                                        (span-end (car item)))
-                    ;; Throw away all commands between start of proof
-                    ;; and the current point, in particular, delete
-                    ;; all the spans.
-                    (mapc
-                     (lambda (item) (span-detach (car item)))
-                     maybe-result)
+                  (progn
+                    (push (list 'proof
+                                (cons item maybe-result)
+                                proof-start-span-start
+                                proof-start-span-end)
+                          result-chunks)
                     (setq maybe-result nil)
-                    ;; Record start and end point for the fancy
-                    ;; colored span that marks the skipped proof. The
-                    ;; span will be created in
-                    ;; `proof-done-advancing-save' when
-                    ;; `proof-script-proof-admit-command' is retired.
-                    (span-set-property
-                     cmd-span 'omitted-proof-region
-                     ;; for the start take proper line start if possible
-                     (list (proof-move-over-whitespace-to-next-line
-                            proof-start-span-start)
-                           ;; For the end, don't extend to the end of
-                           ;; the line, because then the fancy color
-                           ;; span is behind the end of the proof span
-                           ;; and will get deleted when undoing just
-                           ;; behind that proof.
-                           (span-end (car item))))
-                    (push (list cmd-span
-                                (list proof-script-proof-admit-command)
-                                'proof-done-advancing nil)
-                          result)
                     (setq inside-proof nil))
 
                 ;; else - no nested proof, no opaque proof, but still inside
@@ -2119,7 +2136,9 @@ start is found inside a proof."
                     ;; such that the proof-must-be-kept.
                     ;; Need to keep all commands from the start of the proof.
                     (progn
-                      (setq result (cons item (nconc maybe-result result)))
+                      (push (list 'no-proof
+                                  (cons item maybe-result))
+                            result-chunks)
                       (setq maybe-result nil)
                       (setq inside-proof nil))
 
@@ -2139,9 +2158,12 @@ start is found inside a proof."
         ;; else - outside proof
         (if (string-match proof-script-proof-start-regexp cmd)
             (progn
+              (push (list 'no-proof
+                          ;; Keep the Proof using command in the
+                          ;; 'no-proof chunk.
+                          (cons item maybe-result))
+                    result-chunks)
               (setq maybe-result nil)
-              ;; Keep the Proof using command in any case.
-              (push item result)
               (setq proof-start-span-start (span-start (car item)))
               (setq proof-start-span-end (span-end (car item)))
               (setq inside-proof t)
@@ -2157,12 +2179,105 @@ start is found inside a proof."
               (setq next-proof-must-be-kept nil)))
 
           ;; keep current item unmodified
-          (push item result)))
+          (push item maybe-result)))
       (setq vanillas (cdr vanillas)))
 
-    ;; end of loop - return filtered vanillas
-    (nreverse (nconc maybe-result result))))
+    ;; end of loop - keep remaining items
+    (when maybe-result
+      (push (list 'no-proof maybe-result) result-chunks))
+    result-chunks))
 
+(defun proof-script-omit-proofs (vanillas)
+  "Return a copy of VANILLAS with complete opaque proofs omitted.
+See `proof-omit-proofs-configured' for the description of the
+omit proofs feature. This function uses
+`proof-script-proof-start-regexp',
+`proof-script-proof-end-regexp' and
+`proof-script-definition-end-regexp' to search for complete
+opaque proofs in the action list VANILLAS. Additionally, it uses
+`proof-script-cmd-prevents-proof-omission' and
+`proof-script-cmd-force-next-proof-kept' to detect proofs that
+cannot be omitted. Complete opaque proofs are replaced by
+`proof-script-proof-admit-command'. The span of the admit command
+contains an 'omitted-proof-region property with the region of the
+omitted proof. This is used in `proof-done-advancing-save' to
+colour the omitted proof with `proof-omitted-proof-face'.
+
+Display a warning if another proof start is found inside a
+proof."
+  (let ((chunks (proof-script-omit-filter vanillas))
+        result)
+    (dolist (chunk chunks result)
+      (cond
+       ((eq (car chunk) 'nested-proof)
+        ;; chunk: ('nested-proof line-number-nested-proof cmds-reversed)
+        ;;
+        ;; A nested-proof chunk can only appear at the head when
+        ;; result is still empty.
+        (cl-assert (null result) nil
+                   "proof-script-omit internal error: nested-proof not at head")
+        ;; Display a warning and keep the commands unmodified.
+        ;;
+        ;; For Coq nobody will notice the warning, because the error
+        ;; about nested proofs will pop up shortly afterwards.
+        (display-warning
+         '(proof-script)
+         ;; use the end of the span, because the start is
+         ;; usually on the preceding  line
+         (format (concat "found second proof start at line %d"
+                         " - are there nested proofs?")
+                 (nth 2 chunk)))
+        (setq result (nreverse (nth 1 chunk))))
+
+       ((eq (car chunk) 'no-proof)
+        ;; chunk: ('no-proof cmds-reversed)
+        ;;
+        ;; keep all commands unmodified
+        (setq result (nconc (nreverse (nth 1 chunk)) result)))
+
+       ((eq (car chunk) 'proof)
+        ;; chunk: ('proof span-start-first-proof-cmd
+        ;;                span-end-first-proof-cmd
+        ;;                proof-cmds-reversed)
+        (let* ((cmds-rev (nth 1 chunk))
+               (proof-start-span-start (nth 2 chunk))
+               (proof-start-span-end (nth 3 chunk))
+               
+               (last-cmd-span (caar cmds-rev)))
+          ;; Reuse the span of the last proof command (Qed) for the
+          ;; whole proof, including the faked Admitted.
+          (span-set-property last-cmd-span 'type 'omitted-proof)
+          (span-set-property last-cmd-span 'cmd proof-script-proof-admit-command)
+          (span-set-endpoints last-cmd-span
+                              proof-start-span-end
+                              (span-end last-cmd-span))
+          ;; Commands inside the proof are thrown away. Thererfore
+          ;; delete all their spans, except the span of the last proof
+          ;; command, which is reused here.
+          (mapc
+           (lambda (item) (span-detach (car item)))
+           (cdr cmds-rev))
+          ;; Record start and end point for the fancy colored span
+          ;; that marks the skipped proof. The span will be created in
+          ;; `proof-done-advancing-save' when
+          ;; `proof-script-proof-admit-command' is retired.
+          (span-set-property
+           last-cmd-span 'omitted-proof-region
+           (list
+            ;; for the start take proper line start if possible
+            (proof-move-over-whitespace-to-next-line proof-start-span-start)
+            ;; For the end, don't extend to the end of the line,
+            ;; because then the fancy color span is behind the end of
+            ;; the proof span and will get deleted when undoing just
+            ;; behind that proof.
+            (span-end last-cmd-span)))
+          ;; replace proof commands by admit
+          (push (list last-cmd-span (list proof-script-proof-admit-command)
+                      'proof-done-advancing nil)
+                result)))
+       (t
+        (cl-assert nil nil
+                   "proof-script-omit internal error: unknown chunk type"))))))
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;