diff --git a/.github/workflows/proof_tools.yml b/.github/workflows/proof_tools.yml
index 66b1f2c76161df073df5cae6bbfaea2d73809423..f219314ab1d499769e5da85ed17cbf5a7834fef4 100644
--- a/.github/workflows/proof_tools.yml
+++ b/.github/workflows/proof_tools.yml
@@ -21,7 +21,7 @@ jobs:
         (cd dopth || exit 1
          opam switch create . --packages dune --yes
          eval $(opam env)
-         dune build) # TODO implement tests
+         bmake tests)
         (cd chainprops || exit 1
          opam switch create . --deps-only --yes
          eval $(opam env)
diff --git a/proofs/dopth/Makefile b/proofs/dopth/Makefile
index c3226ed70346397aadce64b1d0d7d007270e550c..6096f165a02e88ab15f6ba6f65f060be0b2c6392 100644
--- a/proofs/dopth/Makefile
+++ b/proofs/dopth/Makefile
@@ -9,4 +9,8 @@ _build/default/dopth.exe: dopth.ml
 psnj-dopth: _build/default/dopth.exe
 	@cp -f _build/default/dopth.exe $@
 
+.PHONY: tests
+tests: _build/default/dopth.exe
+	@${DUNE} runtest
+
 .include "../tools.mk"
diff --git a/proofs/dopth/dune-project b/proofs/dopth/dune-project
index c994249ac26f9d7da66508a748d9d7ca4a82a441..ae730292676bfc91a5a5e576cfbc1f333eb7df2d 100644
--- a/proofs/dopth/dune-project
+++ b/proofs/dopth/dune-project
@@ -1 +1,2 @@
 (lang dune 2.9)
+(cram enable)
diff --git a/proofs/dopth/psnj-dopth.asciidoc b/proofs/dopth/psnj-dopth.asciidoc
index 01d86149a83ffde89a608ad9a781968d8a6cc4e0..3b59219fd4f337c635de78f6b3f858b6a917481e 100644
--- a/proofs/dopth/psnj-dopth.asciidoc
+++ b/proofs/dopth/psnj-dopth.asciidoc
@@ -13,7 +13,7 @@ psnj-dopth
 
 *psnj-dopth* is a filter that transform a newline-separated list
 of strings and paths into a Makefile dependency list. A path is a
-dot-separated list of integers (such as 0.1.1) or the word _root_. A
+dot-separated list of integers (such as 0.1.1) or the word *root*. A
 string _s1_ depends on a string _s2_ if the path of _s1_ is a successor
 of the path of _s2_.  A path _p_ is a successor of _q_ if _p_ = _q_.i
 where _i_ is an integer.
@@ -37,7 +37,7 @@ frob
 1
 ----
 
-dopth returns
+dopth returns (the order is not specified)
 
 ----
 foo: bar frob
diff --git a/proofs/dopth/tests/dopth.t b/proofs/dopth/tests/dopth.t
new file mode 100644
index 0000000000000000000000000000000000000000..d4d4b0aa5ef1b86e017640ab342770f371d2cdc6
--- /dev/null
+++ b/proofs/dopth/tests/dopth.t
@@ -0,0 +1,3 @@
+  $ ../dopth.exe < example.plain
+  bar: baz
+  foo: bar frob
diff --git a/proofs/dopth/tests/dune b/proofs/dopth/tests/dune
new file mode 100644
index 0000000000000000000000000000000000000000..792f222562bbcd160e2b5e56de8610c6b19a5d54
--- /dev/null
+++ b/proofs/dopth/tests/dune
@@ -0,0 +1,4 @@
+(cram
+ (deps
+  ../dopth.exe
+  example.plain))
diff --git a/proofs/dopth/tests/example.plain b/proofs/dopth/tests/example.plain
new file mode 100644
index 0000000000000000000000000000000000000000..0c269530b0cdb6cccdb43f0462871b0e1e6e7ca2
--- /dev/null
+++ b/proofs/dopth/tests/example.plain
@@ -0,0 +1,8 @@
+foo
+root
+bar
+0
+baz
+0.1
+frob
+1