diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index eaacac9..76fefaf 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -18,7 +18,7 @@ jobs:
           - 'coqorg/coq:dev'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - uses: coq-community/docker-coq-action@v1
         with:
           custom_image: ${{ matrix.image }}
@@ -42,7 +42,17 @@ jobs:
               opam install -y -v -j 2 coq-stalmarck-tactic
               opam list
             endGroup
+            startGroup "Build stalmarck-checker dependencies"
+              opam pin add -n -y -k path coq-stalmarck-checker .
+              opam update -y
+              opam install -y -j 2 coq-stalmarck-checker --deps-only
+            endGroup
+            startGroup "Build stalmarck-checker"
+              opam install -y -v -j 2 coq-stalmarck-checker
+              opam list
+            endGroup
             startGroup "Uninstallation test"
+              opam remove -y coq-stalmarck-checker
               opam remove -y coq-stalmarck-tactic
               opam remove -y coq-stalmarck
             endGroup
diff --git a/coq-stalmarck-checker.opam b/coq-stalmarck-checker.opam
new file mode 100644
index 0000000..d90f362
--- /dev/null
+++ b/coq-stalmarck-checker.opam
@@ -0,0 +1,22 @@
+opam-version: "2.0"
+maintainer: "palmskog@gmail.com"
+version: "dev"
+
+homepage: "https://github.com/coq-community/stalmarck"
+dev-repo: "git+https://github.com/coq-community/stalmarck.git"
+bug-reports: "https://github.com/coq-community/stalmarck/issues"
+license: "LGPL-2.1-or-later"
+
+synopsis: "Verified tool for proving tautologies using Stålmarck's algorithm"
+
+build: ["dune" "build" "-p" name "-j" jobs]
+depends: [
+  "ocaml" {>= "4.09.0"}
+  "dune" {>= "2.8"}
+  "coq-stalmarck-tactic" {= version}
+]
+
+authors: [
+  "Pierre Letouzey"
+  "Laurent Théry"
+]
diff --git a/coq-stalmarck-tactic.opam b/coq-stalmarck-tactic.opam
index bd80662..e83519b 100644
--- a/coq-stalmarck-tactic.opam
+++ b/coq-stalmarck-tactic.opam
@@ -7,7 +7,7 @@ dev-repo: "git+https://github.com/coq-community/stalmarck.git"
 bug-reports: "https://github.com/coq-community/stalmarck/issues"
 license: "LGPL-2.1-or-later"
 
-synopsis: "Coq tactic and verified tool for proving tautologies using Stålmarck's algorithm"
+synopsis: "Coq tactic for proving tautologies using Stålmarck's algorithm"
 
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
diff --git a/src/dune b/src/dune
index 92d5fa8..3fce5e2 100644
--- a/src/dune
+++ b/src/dune
@@ -27,4 +27,4 @@
  (public_name stalmarck)
  (libraries coq-stalmarck-tactic.stal unix)
  (modules lexer parser main)
- (package coq-stalmarck-tactic))
+ (package coq-stalmarck-checker))