diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
deleted file mode 100644
index ae8f57cc..00000000
--- a/.github/workflows/build.yml
+++ /dev/null
@@ -1,50 +0,0 @@
-# This is a basic workflow to help you get started with Actions
-
-name: Test build
-
-# Controls when the action will run.
-on:
-  # Triggers the workflow on push or pull request events but only for the main branch
-  push:
-    branches: [ main ]
-  pull_request:
-    branches: [ main ]
-
-  # Allows you to run this workflow manually from the Actions tab
-  workflow_dispatch:
-
-# A workflow run is made up of one or more jobs that can run sequentially or in parallel
-jobs:
-  # This workflow contains a single job called "build"
-  build:
-    # The type of runner that the job will run on
-    runs-on: ubuntu-latest
-
-    # Steps represent a sequence of tasks that will be executed as part of the job
-    steps:
-
-      - name: Try to restore opam cache
-        id: opam-cache
-        uses: actions/cache@v2
-        with:
-          path: "~/.opam"
-          key: opam-${{github.base_ref}}-${{github.ref}}
-          restore-keys: |
-            opam--refs/heads/${{github.base_ref}}
-
-      - name: Install OCaml
-        uses: avsm/setup-ocaml@v1
-        with:
-          ocaml-version: 4.07.1
-
-      # Checks-out your repository under $GITHUB_WORKSPACE, so your job can access it
-      - name: Checkout repo
-        uses: actions/checkout@v2
-
-      # Runs a set of commands using the runners shell
-      - name: Build
-        run: |
-          opam repo add coq-released https://coq.inria.fr/opam/released
-          opam install coq.8.14.0 coq-equations.1.3+8.14 coq-mathcomp-ssreflect.1.13.0 coq-mathcomp-analysis.0.3.13 coq-extructures.0.3.1
-          opam exec -- make -j4
-
diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
new file mode 100644
index 00000000..0d4d08f2
--- /dev/null
+++ b/.github/workflows/docker-action.yml
@@ -0,0 +1,31 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+name: Docker CI
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+    branches:
+      - '**'
+
+jobs:
+  build:
+    # the OS must be GNU/Linux to be able to use the docker-coq-action
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        image:
+          - 'mathcomp/mathcomp:1.13.0-coq-8.14'
+      fail-fast: false
+    steps:
+      - uses: actions/checkout@v2
+      - uses: coq-community/docker-coq-action@v1
+        with:
+          opam_file: 'coq-ssprove.opam'
+          custom_image: ${{ matrix.image }}
+
+# See also:
+# https://github.com/coq-community/docker-coq-action#readme
+# https://github.com/erikmd/docker-coq-github-action-demo
diff --git a/CI.md b/CI.md
new file mode 100644
index 00000000..845ebd0d
--- /dev/null
+++ b/CI.md
@@ -0,0 +1,18 @@
+In this project, continuous integration is based on Github Actions.
+For now we rely on https://github.com/coq-community/templates to generate
+the action from the `meta.yml` file. Actually the `coq-ssprove.opam` file is
+also generated from it.
+
+## With bash
+
+```bash
+TMP=$(mktemp -d); git clone https://github.com/coq-community/templates.git $TMP
+$TMP/generate.sh .github/workflows/docker-action.yml coq-ssprove.opam
+```
+
+## With fish
+
+```fish
+set TMP (mktemp -d) ; git clone https://github.com/coq-community/templates.git $TMP
+$TMP/generate.sh .github/workflows/docker-action.yml coq-ssprove.opam
+```
\ No newline at end of file
diff --git a/coq-ssprove.opam b/coq-ssprove.opam
new file mode 100644
index 00000000..b7c90025
--- /dev/null
+++ b/coq-ssprove.opam
@@ -0,0 +1,42 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+opam-version: "2.0"
+maintainer: "philipp@haselwarter.org"
+version: "dev"
+
+homepage: "https://github.com/ssprove/ssprove"
+dev-repo: "git+https://github.com/ssprove/ssprove.git"
+bug-reports: "https://github.com/ssprove/ssprove/issues"
+license: "MIT"
+
+synopsis: "A framework for modular crypto proofs"
+description: """
+This repository contains a library for doing both state separating proofs
+(SSP) and for showing low-level equivalences of probabilistic stateful
+programs."""
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "coq" {>= "8.14"}
+  "coq-mathcomp-ssreflect" {(>= "1.13.0" & < "1.14~")}
+  "coq-mathcomp-analysis" {= "0.3.13"}
+  "coq-equations" {>= "1.3"}
+  "coq-extructures" {(>= "0.3.1" & < "dev")}
+]
+
+tags: [
+  "logpath:"
+]
+authors: [
+  "Carmine Abate"
+  "Philipp G. Haselwarter"
+  "Exequiel Rivas"
+  "Antoine Van Muylder"
+  "Théo Winterhalter"
+  "Nikolaj Sidorenco"
+  "Cătălin Hrițcu"
+  "Kenji Maillard"
+  "Bas Spitters"
+]
diff --git a/meta.yml b/meta.yml
new file mode 100644
index 00000000..c9d65f14
--- /dev/null
+++ b/meta.yml
@@ -0,0 +1,65 @@
+fullname: SSProve framework
+shortname: ssprove
+organization: ssprove
+opam_name: coq-ssprove
+community: false
+action: true
+coqdoc: false
+branch: main
+
+synopsis: >-
+  A framework for modular crypto proofs
+description: |-
+  This repository contains a library for doing both state separating proofs
+  (SSP) and for showing low-level equivalences of probabilistic stateful
+  programs.
+authors:
+- name: Carmine Abate
+  initial: true
+- name: Philipp G. Haselwarter
+  initial: true
+- name: Exequiel Rivas
+  initial: true
+- name: Antoine Van Muylder
+  initial: true
+- name: Théo Winterhalter
+  initial: true
+- name: Nikolaj Sidorenco
+  initial: false
+- name: Cătălin Hrițcu
+  initial: true
+- name: Kenji Maillard
+  initial: true
+- name: Bas Spitters
+  initial: true
+
+opam-file-maintainer: philipp@haselwarter.org
+
+opam-file-version: dev
+
+license:
+  fullname: MIT
+  identifier: MIT
+  file: LICENSE
+
+supported_coq_versions:
+  text: Coq 8.14
+  opam: '{>= "8.14"}'
+
+tested_coq_opam_versions:
+- version: '1.13.0-coq-8.14'
+  repo: 'mathcomp/mathcomp'
+
+dependencies:
+- opam:
+    name: coq-mathcomp-ssreflect
+    version: '{(>= "1.13.0" & < "1.14~")}'
+- opam:
+    name: coq-mathcomp-analysis
+    version: '{= "0.3.13"}'
+- opam:
+    name: coq-equations
+    version: '{>= "1.3"}'
+- opam:
+    name: coq-extructures
+    version: '{(>= "0.3.1" & < "dev")}'
diff --git a/ssprove.opam b/ssprove.opam
deleted file mode 100644
index 97f69700..00000000
--- a/ssprove.opam
+++ /dev/null
@@ -1,22 +0,0 @@
-opam-version: "2.0"
-name: "ssprove"
-version: "dev"
-synopsis: "A Foundational Framework for Modular Cryptographic Proofs"
-maintainer: "philipp@haselwarter.org"
-authors: ["SSProve team"]
-homepage: "https://github.com/SSProve/ssprove"
-bug-reports: "https://github.com/SSProve/ssprove/issues"
-license: "MIT"
-depends: [
-  "coq" {>= "8.14"}
-  "coq-equations" {>= "1.3"}
-  "coq-mathcomp-ssreflect" {(>= "1.13.0" & < "1.14~")}
-  "coq-mathcomp-analysis" {= "0.3.13"}
-  "coq-extructures" {(>= "0.3.1" & < "dev")}
-]
-build: [
-  [make "-j%{jobs}%"]
-]
-install: [
-  [make "install"]
-]