diff --git a/.woodpecker.yaml b/.woodpecker.yaml
new file mode 100644
index 0000000..c121f1b
--- /dev/null
+++ b/.woodpecker.yaml
@@ -0,0 +1,13 @@
+when:
+  - event: [push, pull_request]
+    branch: [main]
+
+steps:
+  - name: build
+    image: coqorg/coq:8.20.1-ocaml-4.14.2-flambda
+    commands:
+      - opam update
+      - opam install -y coq-hammer-tactics coq-equations coq-stdpp coq-autosubst-ocaml
+      - eval $(opam env)
+      - sudo chown -R 1000:1000 .
+      - make -j2
diff --git a/README.org b/README.org
index 69c5993..8685d8b 100644
--- a/README.org
+++ b/README.org
@@ -1,4 +1,6 @@
 * Church Rosser, surjective pairing, and strong normalization
+[![status-badge](https://woodpecker.electriclam.com/api/badges/3/status.svg)](https://woodpecker.electriclam.com/repos/3)
+
 This repository contains a mechanized proof that the lambda calculus
 with beta and eta rules for functions and pairs is in fact confluent
 for the subset of terms that are "strongly $\beta$-normalizing".