diff --git a/checker/dune b/checker/dune
index 32bbcd240af1..3000d289abf4 100644
--- a/checker/dune
+++ b/checker/dune
@@ -6,7 +6,7 @@
  (name coq_checklib)
  (public_name rocq-runtime.checklib)
  (synopsis "Rocq's Standalone Proof Checker")
- (modules :standard \ coqchk votour)
+ (modules :standard \ rocqchk coqchk votour)
  (wrapped true)
  (libraries rocq-runtime.boot rocq-runtime.kernel))
 
@@ -14,12 +14,20 @@
  (old_public_name coq-core.checklib)
  (new_public_name rocq-runtime.checklib))
 
+(executable
+ (name rocqchk)
+ (public_name rocqchk)
+ (modes exe byte)
+ (package rocq-runtime)
+ (modules rocqchk)
+ (flags :standard -open Coq_checklib)
+ (libraries coq_checklib))
+
 (executable
  (name coqchk)
  (public_name coqchk)
  (modes exe byte)
- ; Move to coq-checker?
- (package rocq-runtime)
+ (package coq-core)
  (modules coqchk)
  (flags :standard -open Coq_checklib)
  (libraries coq_checklib))
diff --git a/checker/rocqchk.ml b/checker/rocqchk.ml
new file mode 100644
index 000000000000..5485e0539019
--- /dev/null
+++ b/checker/rocqchk.ml
@@ -0,0 +1,2 @@
+
+let () = Coqchk_main.main ()
diff --git a/checker/rocqchk.mli b/checker/rocqchk.mli
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/topbin/rocq.ml b/topbin/rocq.ml
index 33335a0087a9..3d6d2a5269f5 100644
--- a/topbin/rocq.ml
+++ b/topbin/rocq.ml
@@ -23,6 +23,12 @@ let with_worker_gen opts basename args =
 let with_worker opts kind args =
   with_worker_gen opts "coqworker" (("--kind="^kind) :: args)
 
+let with_sibling_exe opts prog args =
+  let prog = System.get_toplevel_path prog in
+  let () = if opts.Rocqshim.debug_shim then Printf.eprintf "Using %s\n%!" prog in
+  let argv = Array.of_list (prog :: args) in
+  Rocqshim.exec_or_create_process prog argv
+
 let () =
   if Array.length Sys.argv < 2 then error_usage ();
 
@@ -38,6 +44,9 @@ let () =
   | ("top-with-drop"|"repl-with-drop") :: args -> with_worker_gen opts "coqworker_with_drop" args
   | "native-precompile" :: args -> with_worker_gen opts "rocqnative" args
 
+  (* public executables *)
+  | "check" :: args -> with_sibling_exe opts "rocqchk" args
+
   (* statically linked subcommands *)
   | ("preprocess-mlg"|"pp-mlg") :: args -> Coqpp_main.main args
   | "dep" :: args -> Coqdeplib.Rocqdep_main.main args