diff --git a/.circleci/config.yml b/.circleci/config.yml
index 8921753814d1..14c102ceded6 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -85,6 +85,9 @@ jobs:
   coquelicot:
     <<: *ci-template
 
+  cross-crypto:
+    <<: *ci-template
+
   elpi:
     <<: *ci-template
 
@@ -160,6 +163,7 @@ workflows:
       - compcert: *req-main
       - coq-dpdgraph: *req-main
       - coquelicot: *req-main
+      - cross-crypto: *req-main
       - elpi: *req-main
       - equations: *req-main
       - geocoq: *req-main
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 1789846c8342..ac4304da1308 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -242,6 +242,9 @@ ci-coq-dpdgraph:
 ci-coquelicot:
   <<: *ci-template
 
+ci-cross-crypto:
+  <<: *ci-template
+
 ci-elpi:
   <<: *ci-template
 
diff --git a/.travis.yml b/.travis.yml
index eeb0b800e918..0f637103eb47 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -74,6 +74,9 @@ matrix:
     - if: NOT (type = pull_request)
       env:
       - TEST_TARGET="ci-coquelicot"
+    - if: NOT (type = pull_request)
+      env:
+      - TEST_TARGET="ci-cross-crypto"
     - if: NOT (type = pull_request)
       env:
       - TEST_TARGET="ci-elpi" EXTRA_OPAM="elpi"
diff --git a/Makefile.ci b/Makefile.ci
index 4d4f1df59a6c..ce725d19dd1e 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -15,6 +15,7 @@ CI_TARGETS=ci-bignums \
     ci-coquelicot \
     ci-corn \
     ci-cpdt \
+    ci-cross-crypto \
     ci-elpi \
     ci-equations \
     ci-fcsl-pcm \
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 1ae2ad0acb96..b7faea13ed20 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -90,6 +90,12 @@
 : "${VST_CI_BRANCH:=master}"
 : "${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git}"
 
+########################################################################
+# cross-crypto
+########################################################################
+: "${cross_crypto_CI_BRANCH:=master}"
+: "${cross_crypto_CI_GITURL:=https://github.com/mit-plv/cross-crypto.git}"
+
 ########################################################################
 # fiat_parsers
 ########################################################################
diff --git a/dev/ci/ci-cross-crypto.sh b/dev/ci/ci-cross-crypto.sh
new file mode 100755
index 000000000000..a0d3aa655176
--- /dev/null
+++ b/dev/ci/ci-cross-crypto.sh
@@ -0,0 +1,11 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+cross_crypto_CI_DIR="${CI_BUILD_DIR}/cross-crypto"
+
+git_checkout "${cross_crypto_CI_BRANCH}" "${cross_crypto_CI_GITURL}" "${cross_crypto_CI_DIR}"
+( cd "${cross_crypto_CI_DIR}" && git submodule update --init --recursive )
+
+( cd "${cross_crypto_CI_DIR}" && make )