diff --git a/.github/workflows/proof_tools.yml b/.github/workflows/proof_tools.yml
index 88e04f6193ad92ab76c62c3720edbd0f6ebe9065..11baf1ddfba1fe6eda1044934e992c2459872491 100644
--- a/.github/workflows/proof_tools.yml
+++ b/.github/workflows/proof_tools.yml
@@ -57,11 +57,11 @@ jobs:
         opam install yojson angstrom feather cmdliner
         cd proofs || exit 1
         (cd split && bmake && sudo bmake install)
-        (cd pipeline && bmake && sudo bmake install)
         (cd psnj_toolbox && make && sudo make install)
+        (cd pipeline && bmake && sudo bmake install)
 
     - name: launch pipeline
       run: |
         cd proofs/pipeline || exit 1
-        bmake tests
+        opam exec -- dune runtest
 
diff --git a/proofs/pipeline/examples/Makefile b/proofs/pipeline/examples/Makefile
deleted file mode 100644
index d3b91a482d0de8ad0aaeb40f5e80b56c657315ed..0000000000000000000000000000000000000000
--- a/proofs/pipeline/examples/Makefile
+++ /dev/null
@@ -1,15 +0,0 @@
-all: test
-	
-run.out: run.sh
-	sh run.sh > run.out
-
-test: run.out run.expected
-	@diff run.expected run.out
-
-promote:
-	cp run.out run.expected
-
-clean: run.out
-
-.PHONY: test diff promote clean all
-
diff --git a/proofs/pipeline/examples/hello/dune b/proofs/pipeline/examples/hello/dune
new file mode 100644
index 0000000000000000000000000000000000000000..d4ad576487c93bf2fe6b49e3159b7d3ab8954a5d
--- /dev/null
+++ b/proofs/pipeline/examples/hello/dune
@@ -0,0 +1,8 @@
+(test
+ (deps
+  hello.log
+  lambdapi.pkg
+  (glob_files encoding/*)
+  (glob_files spec/main.lp))
+ (name hello)
+ (libraries unix))
diff --git a/proofs/pipeline/examples/hello/encoding b/proofs/pipeline/examples/hello/encoding
new file mode 120000
index 0000000000000000000000000000000000000000..efb722e95c94f0ffaf1f53395e55bb1220736dc3
--- /dev/null
+++ b/proofs/pipeline/examples/hello/encoding
@@ -0,0 +1 @@
+../encoding/
\ No newline at end of file
diff --git a/proofs/pipeline/examples/run.expected b/proofs/pipeline/examples/hello/hello.expected
similarity index 100%
rename from proofs/pipeline/examples/run.expected
rename to proofs/pipeline/examples/hello/hello.expected
diff --git a/proofs/pipeline/examples/hello.log b/proofs/pipeline/examples/hello/hello.log
similarity index 100%
rename from proofs/pipeline/examples/hello.log
rename to proofs/pipeline/examples/hello/hello.log
diff --git a/proofs/pipeline/examples/hello/hello.ml b/proofs/pipeline/examples/hello/hello.ml
new file mode 100644
index 0000000000000000000000000000000000000000..b57cf875d53fdaacc3cbb6ed5746124c86757fa1
--- /dev/null
+++ b/proofs/pipeline/examples/hello/hello.ml
@@ -0,0 +1,13 @@
+let () =
+  match
+    Unix.system
+      (Filename.quote_command "psnj-pipe"
+         [ "--qfo"; "encoding/qfo.json"; "hello.log" ])
+  with
+  | Unix.WEXITED 0 -> exit 0
+  | Unix.WEXITED n ->
+      Format.eprintf "Command exited with code %d@." n;
+      exit 1
+  | Unix.WSIGNALED _ | Unix.WSTOPPED _ ->
+      Format.eprintf "Command stopped by signal";
+      exit 2
diff --git a/proofs/pipeline/examples/hello.prf b/proofs/pipeline/examples/hello/hello.prf
similarity index 100%
rename from proofs/pipeline/examples/hello.prf
rename to proofs/pipeline/examples/hello/hello.prf
diff --git a/proofs/pipeline/examples/hello.pvs b/proofs/pipeline/examples/hello/hello.pvs
similarity index 100%
rename from proofs/pipeline/examples/hello.pvs
rename to proofs/pipeline/examples/hello/hello.pvs
diff --git a/proofs/pipeline/examples/hello/lambdapi.pkg b/proofs/pipeline/examples/hello/lambdapi.pkg
new file mode 120000
index 0000000000000000000000000000000000000000..3b1336c4b1e320b07e7d1e13bc3dd643f334c339
--- /dev/null
+++ b/proofs/pipeline/examples/hello/lambdapi.pkg
@@ -0,0 +1 @@
+../lambdapi.pkg
\ No newline at end of file
diff --git a/proofs/pipeline/examples/hello/spec/main.lp b/proofs/pipeline/examples/hello/spec/main.lp
new file mode 100644
index 0000000000000000000000000000000000000000..c4cfc952b8f6bbcc30502121a2f1825d9c7c4b18
--- /dev/null
+++ b/proofs/pipeline/examples/hello/spec/main.lp
@@ -0,0 +1,3 @@
+require open qfo.encoding.lhol qfo.encoding.pvs_cert;
+symbol P: Prop;
+symbol Q: Prop;
diff --git a/proofs/pipeline/examples/run.sh b/proofs/pipeline/examples/run.sh
deleted file mode 100644
index 7f052f849945a6a3679945edaa53cf055374a41d..0000000000000000000000000000000000000000
--- a/proofs/pipeline/examples/run.sh
+++ /dev/null
@@ -1,3 +0,0 @@
-#!/bin/sh
-set -euf
-opam exec -- psnj-pipe --qfo=encoding/qfo.json hello.log