diff --git a/.gitignore b/.gitignore
index e51be4e98184794797f37b115e34e10c3789a1ee..ac80ddd41919392c2046224c30b75a8134be597b 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,5 @@
 *.lpo
 log-lp.txt
 log-lsp.txt
+_build/
+_opam/
diff --git a/proofs/appaxiom/.gitignore b/proofs/appaxiom/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..27d8084067096606ee10d0d194aa793ef4374c72
--- /dev/null
+++ b/proofs/appaxiom/.gitignore
@@ -0,0 +1 @@
+psnj-appaxiom
diff --git a/proofs/pipeline/.gitignore b/proofs/pipeline/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..4fed5a39c9266175e14c48640dbd27ecafc3d17c
--- /dev/null
+++ b/proofs/pipeline/.gitignore
@@ -0,0 +1 @@
+psnj-pipe
diff --git a/proofs/pipeline/.ocamlformat b/proofs/pipeline/.ocamlformat
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/proofs/pipeline/Makefile b/proofs/pipeline/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..0f9eb4ef26648ed6ef5c9363adfc9ff8527c6f70
--- /dev/null
+++ b/proofs/pipeline/Makefile
@@ -0,0 +1,5 @@
+ROOT     = pipe
+CMDLINER = true
+
+.include "../dune-exe.mk"
+.include "../tools.mk"
diff --git a/proofs/dkproof.mk b/proofs/pipeline/dkproof.mk
similarity index 100%
rename from proofs/dkproof.mk
rename to proofs/pipeline/dkproof.mk
diff --git a/proofs/pipeline/dune b/proofs/pipeline/dune
new file mode 100644
index 0000000000000000000000000000000000000000..147e7be94cc922e9a638d4a804de0c8bc70439bd
--- /dev/null
+++ b/proofs/pipeline/dune
@@ -0,0 +1,3 @@
+(executable
+ (name pipe)
+ (libraries feather cmdliner))
diff --git a/proofs/pipeline/dune-project b/proofs/pipeline/dune-project
new file mode 100644
index 0000000000000000000000000000000000000000..66612c7a8450214f06cf46f11622cdea5bd13fc3
--- /dev/null
+++ b/proofs/pipeline/dune-project
@@ -0,0 +1,8 @@
+(lang dune 2.9)
+(name psnj_pipe)
+(generate_opam_files true)
+
+(package
+ (name psnj_pipe)
+ (synopsis "Pipeline for personoj")
+ (depends cmdliner feather))
diff --git a/proofs/pipeline/pipe.ml b/proofs/pipeline/pipe.ml
new file mode 100644
index 0000000000000000000000000000000000000000..7204242e7541a355dbcc8a14986c40e7ff0324d8
--- /dev/null
+++ b/proofs/pipeline/pipe.ml
@@ -0,0 +1,50 @@
+open Feather
+open Feather.Infix
+
+let process src proveit qfo_conf =
+  (* Define commands *)
+  let proveit = process proveit [ "--traces"; "-l"; src ]
+  and keepjson = process "perl" [ "-ne"; "print if /^\\{.*\\}$/" ]
+  and mkprops =
+    process "jq"
+      [
+        "-r";
+        {d|"symbol {|" + .name + "!" + (.incr | tostring) + "|}: " + .dk + ";"|d};
+      ]
+  and mkdeps =
+    process "jq" [ "-r"; {|(.name + "!" + (.incr | tostring)), .path|} ]
+  and dopth = process "dopth" []
+  and chainprops depfile = process "psnj-chainprops" [ depfile ]
+  and foise = process "psnj-qfo" [qfo_conf] in
+  let logfile = Filename.remove_extension src ^ ".log" in
+  let depfile = Filename.(temp_file (remove_extension src) ".dep") in
+  (* Run commands *)
+  run (proveit > "/dev/null");
+  let json = collect stdout (cat logfile |. keepjson) in
+  run (echo json |. mkdeps |. dopth > depfile);
+  let propositions =
+    collect stdout (echo json |. mkprops |. chainprops depfile |. foise)
+  in
+  Format.printf "%s" propositions
+
+open Cmdliner
+
+let src =
+  let doc = "Rerun proofs of file $(docv) and record log" in
+  Arg.(required & pos 0 (some string) None & info [] ~doc ~docv:"PVS")
+
+let proveit =
+  let doc = "Path to the proveit script" in
+  Arg.(value & opt string "proveit" & info [ "proveit" ] ~doc)
+
+let qfo_conf =
+  let doc = "Configuration for QFO" in
+  Arg.(value & opt string "qfo.json" & info [ "qfo" ] ~doc)
+
+let cmd =
+  let exits = Term.default_exits in
+  let doc = "Pipeline for personoj" in
+  ( Term.(const process $ src $ proveit $ qfo_conf),
+    Term.(info "psnj-pipe" ~exits ~doc) )
+
+let () = Term.(exit @@ eval cmd)
diff --git a/proofs/pipeline/psnj_pipe.opam b/proofs/pipeline/psnj_pipe.opam
new file mode 100644
index 0000000000000000000000000000000000000000..860fe2a4d4090959e2a0b4b88f057b9f91f49c65
--- /dev/null
+++ b/proofs/pipeline/psnj_pipe.opam
@@ -0,0 +1,25 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "Pipeline for personoj"
+depends: [
+  "dune" {>= "2.9"}
+  "cmdliner"
+  "feather"
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "--promote-install-files=false"
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+  ["dune" "install" "-p" name "--create-install-files" name]
+]
diff --git a/specs/tools/prelude/.gitignore b/specs/tools/prelude/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..f4f176692c7d38e6a173ce1ad5643da2bcfa3887
--- /dev/null
+++ b/specs/tools/prelude/.gitignore
@@ -0,0 +1,2 @@
+number_fields.lp.orig
+number_fields.lp.rej