diff --git a/.cirrus.yml b/.cirrus.yml
index 1aab9e64..9a97e2dd 100644
--- a/.cirrus.yml
+++ b/.cirrus.yml
@@ -1,7 +1,7 @@
 ---
-cirrus-ci_task:
+bazel-release_task:
   container:
-    image: toxchat/toktok-stack:0.0.31-third_party
+    image: toxchat/toktok-stack:0.0.31-release
     cpu: 2
     memory: 2G
   configure_script:
@@ -19,7 +19,7 @@ cirrus-ci_task:
 
 cimple_task:
   container:
-    image: toxchat/toktok-stack:0.0.31-third_party
+    image: toxchat/toktok-stack:0.0.31-release
     cpu: 2
     memory: 4G
   configure_script:
diff --git a/.github/settings.yml b/.github/settings.yml
index 87e46041..c2e5af16 100644
--- a/.github/settings.yml
+++ b/.github/settings.yml
@@ -13,11 +13,12 @@ branches:
       required_status_checks:
         contexts:
           - build-bootstrapd-docker
+          - build-compcert
           - build-macos
           - build-nacl
+          - build-tcc
           - build-win32
           - build-win64
-          - Codacy Static Code Analysis
           - CodeFactor
           - "ci/circleci: asan"
           - "ci/circleci: clang-tidy"
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 9c00a2fd..e10a209a 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -51,3 +51,54 @@ jobs:
       - uses: actions/checkout@v2
       - name: Build and test
         run: .travis/cmake-osx
+
+  build-tcc:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v2
+      - name: Install dependencies
+        run:
+          sudo apt-get install -y --no-install-recommends
+            tcc
+            libconfig-dev
+            libopus-dev
+            libsodium-dev
+            libvpx-dev
+      - name: Build with TCC
+        run:
+          tcc
+            -o send_message_test
+            -Wall -Werror
+            -bench -g
+            auto_tests/send_message_test.c
+            testing/misc_tools.c
+            toxav/*.c
+            toxcore/*.c
+            toxencryptsave/*.c
+            $(pkg-config --cflags --libs libsodium opus vpx)
+      - name: Run the test
+        run: "./send_message_test | grep 'tox clients connected'"
+
+  build-compcert:
+    runs-on: ubuntu-latest
+    container: toxchat/compcert
+    steps:
+      - uses: actions/checkout@v2
+      - name: Build with CompCert
+        run:
+          ccomp
+            -o send_message_test
+            -Wall -Werror
+            -Wno-c11-extensions
+            -Wno-unknown-pragmas
+            -Wno-unused-variable
+            -fstruct-passing -fno-unprototyped -g
+            auto_tests/send_message_test.c
+            testing/misc_tools.c
+            toxav/*.c
+            toxcore/*.c
+            toxencryptsave/*.c
+            -D__COMPCERT__ -DDISABLE_VLA
+            -lpthread $(pkg-config --cflags --libs libsodium opus vpx)
+      - name: Run the test
+        run: "./send_message_test | grep 'tox clients connected'"
diff --git a/other/bootstrap_daemon/docker/tox-bootstrapd.sha256 b/other/bootstrap_daemon/docker/tox-bootstrapd.sha256
index 6d0ea00c..765960a1 100644
--- a/other/bootstrap_daemon/docker/tox-bootstrapd.sha256
+++ b/other/bootstrap_daemon/docker/tox-bootstrapd.sha256
@@ -1 +1 @@
-7cce630be98faab64c804255e060c85a63ea9f4401ffd1f12122ba1c5cfc45ce  /usr/local/bin/tox-bootstrapd
+f0f315faebe7fc88b15ba656c5866c3932b5495c23ee99bdac539ba986688c92  /usr/local/bin/tox-bootstrapd
diff --git a/toxcore/ccompat.h b/toxcore/ccompat.h
index 051b2789..f03dbad1 100644
--- a/toxcore/ccompat.h
+++ b/toxcore/ccompat.h
@@ -33,6 +33,11 @@ bool unused_for_tokstyle(void);
 // Emulation using alloca.
 #ifdef _WIN32
 #include <malloc.h>
+#elif defined(__COMPCERT__)
+// TODO(iphydf): This leaks memory like crazy, so compcert is useless for now.
+// Once we're rid of VLAs, we can remove this and compcert becomes useful.
+#define alloca malloc
+#include <stdlib.h>
 #elif defined(__linux__)
 #include <alloca.h>
 #else