diff --git a/.github/workflows/docker-build.yml b/.github/workflows/docker-build.yml
index 8d36e86..fff0a17 100644
--- a/.github/workflows/docker-build.yml
+++ b/.github/workflows/docker-build.yml
@@ -16,10 +16,10 @@ jobs:
     - uses: actions/checkout@v3
     - run: ./build.sh -v -b sel4
     # the following will also build the plain camkes image:
-    - run: ./build.sh -v -b camkes -s cakeml -s cogent -s rust
+    - run: ./build.sh -v -b camkes -s cakeml -s rust
 
-  # This needs to rebuild the seL4 and camkes images (apart from cakeml/cogent/rust),
-  # but putting l4v in the same job as the large camkes-cakeml-cogent-rust image
+  # This needs to rebuild the seL4 and camkes images (apart from cakeml/rust),
+  # but putting l4v in the same job as the large camkes-cakeml-rust image
   # overflows the disk space of the GitHub runner.
   build-l4v:
     name: Docker images (l4v)
diff --git a/.github/workflows/docker-deploy.yml b/.github/workflows/docker-deploy.yml
index a5bec17..140f9cd 100644
--- a/.github/workflows/docker-deploy.yml
+++ b/.github/workflows/docker-deploy.yml
@@ -48,12 +48,12 @@ jobs:
         ./build.sh -e SNAPSHOT_DATE=${SNAPSHOT_DATE} -v -b sel4
         docker tag trustworthysystems/sel4:latest trustworthysystems/sel4:${TAG}
     # the following will also build the plain camkes image:
-    - name: "Build trustworthysystems/camkes-cakeml-cogent-rust"
+    - name: "Build trustworthysystems/camkes-cakeml-rust"
       run: |
-       ./build.sh -e SNAPSHOT_DATE=${SNAPSHOT_DATE} -v -b camkes -s cakeml -s cogent -s rust
+       ./build.sh -e SNAPSHOT_DATE=${SNAPSHOT_DATE} -v -b camkes -s cakeml -s rust
        docker tag trustworthysystems/camkes:latest trustworthysystems/camkes:${TAG}
-       docker tag trustworthysystems/camkes-cakeml-cogent-rust:latest \
-                  trustworthysystems/camkes-cakeml-cogent-rust:${TAG}
+       docker tag trustworthysystems/camkes-cakeml-rust:latest \
+                  trustworthysystems/camkes-cakeml-rust:${TAG}
 
     - name: Authenticate
       if: ${{ github.repository_owner == 'seL4' }}
@@ -71,13 +71,13 @@ jobs:
         docker push trustworthysystems/camkes:${TAG}
         docker tag trustworthysystems/camkes:${TAG} trustworthysystems/camkes:latest
         docker push trustworthysystems/camkes:latest
-    - name: "Push trustworthysystems/camkes-cakeml-cogent-rust"
+    - name: "Push trustworthysystems/camkes-cakeml-rust"
       if: ${{ github.repository_owner == 'seL4' }}
       run: |
-        docker push trustworthysystems/camkes-cakeml-cogent-rust:${TAG}
-        docker tag trustworthysystems/camkes-cakeml-cogent-rust:${TAG} \
-                   trustworthysystems/camkes-cakeml-cogent-rust:latest
-        docker push trustworthysystems/camkes-cakeml-cogent-rust:latest
+        docker push trustworthysystems/camkes-cakeml-rust:${TAG}
+        docker tag trustworthysystems/camkes-cakeml-rust:${TAG} \
+                   trustworthysystems/camkes-cakeml-rust:latest
+        docker push trustworthysystems/camkes-cakeml-rust:latest
 
   build-l4v:
     name: Docker (l4v)
diff --git a/README.md b/README.md
index 8e90053..b6eec6a 100644
--- a/README.md
+++ b/README.md
@@ -131,7 +131,7 @@ Adding dependencies into the `extras.dockerfile` will build them the next time y
 To build the Dockerfiles locally, you will need to use the included `build.sh` script. It has a help menu:
 
     ./build.sh -h
-        build.sh [-r] -b [sel4|camkes|l4v] -s [binary_decomp|cakeml|camkes_vis|cogent|riscv|rust|sysinit|] -s ... -e MAKE_CACHES=no -e ...
+        build.sh [-r] -b [sel4|camkes|l4v] -s [binary_decomp|cakeml|camkes_vis|riscv|rust|sysinit|] -s ... -e MAKE_CACHES=no -e ...
 
          -r     Rebuild docker images (don't use the docker cache)
          -v     Verbose mode
diff --git a/dockerfiles/apply-cogent.Dockerfile b/dockerfiles/apply-cogent.Dockerfile
deleted file mode 100644
index d93a3c7..0000000
--- a/dockerfiles/apply-cogent.Dockerfile
+++ /dev/null
@@ -1,31 +0,0 @@
-#
-# Copyright 2020, Data61/CSIRO
-#
-# SPDX-License-Identifier: BSD-2-Clause
-#
-
-ARG BASE_IMG=trustworthysystems/camkes
-# hadolint ignore=DL3006
-FROM $BASE_IMG
-
-LABEL ORGANISATION="Trustworthy Systems"
-LABEL MAINTAINER="Luke Mondy (luke.mondy@data61.csiro.au)"
-
-# ARGS are env vars that are *only available* during the docker build
-# They can be modified at docker build time via '--build-arg VAR="something"'
-ARG SCM
-ARG DESKTOP_MACHINE=no
-ARG USE_DEBIAN_SNAPSHOT=yes
-ARG MAKE_CACHES=yes
-ARG COGENT_DIR="/cogent"
-
-ARG SCRIPT=apply-cogent.sh
-
-COPY scripts /tmp/
-
-RUN /bin/bash /tmp/${SCRIPT} \
-    && apt-get clean autoclean \
-    && apt-get autoremove --purge --yes \
-    && rm -rf /var/lib/apt/lists/*
-
-ENV PATH "${PATH}:${HOME}/.cogent-sandbox/bin:/opt/ghc/bin:/opt/cabal/bin"
diff --git a/dockerfiles/apply-cogent_verification.Dockerfile b/dockerfiles/apply-cogent_verification.Dockerfile
deleted file mode 100644
index ddf7149..0000000
--- a/dockerfiles/apply-cogent_verification.Dockerfile
+++ /dev/null
@@ -1,28 +0,0 @@
-#
-# Copyright 2020, Data61/CSIRO
-#
-# SPDX-License-Identifier: BSD-2-Clause
-#
-
-ARG BASE_IMG=trustworthysystems/camkes-cogent
-# hadolint ignore=DL3006
-FROM $BASE_IMG
-
-LABEL ORGANISATION="Trustworthy Systems"
-LABEL MAINTAINER="Luke Mondy (luke.mondy@data61.csiro.au)"
-
-# ARGS are env vars that are *only available* during the docker build
-# They can be modified at docker build time via '--build-arg VAR="something"'
-ARG SCM
-ARG DESKTOP_MACHINE=no
-ARG MAKE_CACHES=yes
-ARG COGENT_DIR="/cogent"
-
-ARG SCRIPT=apply-cogent_verification.sh
-
-COPY scripts /tmp/
-
-RUN /bin/bash /tmp/${SCRIPT} \
-    && apt-get clean autoclean \
-    && apt-get autoremove --purge --yes \
-    && rm -rf /var/lib/apt/lists/*
diff --git a/scripts/apply-binary_decomp.sh b/scripts/apply-binary_decomp.sh
index 4af16f6..51ad561 100644
--- a/scripts/apply-binary_decomp.sh
+++ b/scripts/apply-binary_decomp.sh
@@ -13,7 +13,6 @@ test -d "$DIR" || DIR=$PWD
 # shellcheck source=utils/common.sh
 . "$DIR/utils/common.sh"
 
-# Where will cogent libraries go
 : "${SMTSOLVERS_DIR:=/usr/local/smtsolvers}"
 
 possibly_toggle_apt_snapshot
diff --git a/scripts/apply-cogent.sh b/scripts/apply-cogent.sh
deleted file mode 100644
index f725d56..0000000
--- a/scripts/apply-cogent.sh
+++ /dev/null
@@ -1,65 +0,0 @@
-#!/bin/bash
-#
-# Copyright 2020, Data61/CSIRO
-#
-# SPDX-License-Identifier: BSD-2-Clause
-#
-
-set -exuo pipefail
-
-# Source common functions
-DIR="${BASH_SOURCE%/*}"
-test -d "$DIR" || DIR=$PWD
-# shellcheck source=utils/common.sh
-. "$DIR/utils/common.sh"
-
-# Where will cogent libraries go
-: "${COGENT_DIR:=/usr/local/cogent}"
-
-possibly_toggle_apt_snapshot
-
-as_root tee /etc/apt/sources.list.d/cabal.list > /dev/null << EOF
-deb http://downloads.haskell.org/debian buster main
-EOF
-
-as_root apt-key adv --keyserver hkp://keyserver.ubuntu.com:80 --recv-keys BA3CBA3FFE22B574
-as_root apt-get update -q
-as_root apt-get install -y --no-install-recommends \
-    cabal-install-3.2 \
-    ghc-8.6.5 \
-    # end of list
-
-echo "export PATH=\"\$PATH:/opt/ghc/bin:/opt/cabal/bin\"" >> "$HOME/.bashrc"
-export PATH="$PATH:/opt/ghc/bin:/opt/cabal/bin"
-
-# Do cabal things
-cabal v1-update
-cabal v1-install \
-    happy \
-    alex \
-    # end of list
-
-try_nonroot_first git clone --depth=1 https://github.com/NICTA/cogent.git "$COGENT_DIR" || chown_dir_to_user "$COGENT_DIR"
-pushd "$COGENT_DIR/cogent/"
-    cabal new-configure --with-compiler=ghc-8.6.5 --flags="-builtin-arrays -refinement-types -docgent -haskell-backend"
-    cabal new-install --installdir="$HOME/.cabal/bin/" --overwrite-policy=always
-    as_root ln -s "$HOME/.cabal/bin/cogent" /usr/local/bin/cogent
-
-    cogent -v
-    # For now, just put an empty folder where autocorres may go in the future
-    mkdir autocorres
-popd
-
-# Get the linux kernel headers, to build filesystems with
-as_root apt-get update -q
-as_root apt-get install -y --no-install-recommends \
-        linux-headers-amd64 \
-        # end of list
-
-# Get the dir of the kernel headers. Because we're in a container, we can't be sure
-# that the kernel running is the same as the headers, and so can't use uname
-kernel_headers_dir="$(find /usr/src -maxdepth 1 -name 'linux-headers-*amd64' -type d | head -n 1)"
-
-echo "export KERNELDIR=\"$kernel_headers_dir\"" >> "$HOME/.bashrc"
-
-possibly_toggle_apt_snapshot
diff --git a/scripts/apply-cogent_verification.sh b/scripts/apply-cogent_verification.sh
deleted file mode 100644
index fcc6e89..0000000
--- a/scripts/apply-cogent_verification.sh
+++ /dev/null
@@ -1,67 +0,0 @@
-#!/bin/bash
-#
-# Copyright 2020, Data61/CSIRO
-#
-# SPDX-License-Identifier: BSD-2-Clause
-#
-
-set -exuo pipefail
-
-# Source common functions
-DIR="${BASH_SOURCE%/*}"
-test -d "$DIR" || DIR=$PWD
-# shellcheck source=utils/common.sh
-. "$DIR/utils/common.sh"
-
-# Where will cogent libraries go
-: "${COGENT_DIR:=/usr/local/cogent}"
-
-# Autocorres version
-: "${AC_VER:=autocorres-1.6.1}"
-: "${AC_DIR:=$COGENT_DIR/autocorres}"
-
-if [[ ! -d $COGENT_DIR ]]; then
-    echo "No COGENT_DIR found! You need to run the apply-cogent.sh script first!"
-    exit 1
-fi
-
-# Not strictly necessary, but it makes the apt operations in
-# ../dockerfiles/apply-cogent_verification.dockerfile work.
-as_root apt-get update -q
-
-as_root pip3 install --no-cache-dir \
-    ruamel.yaml \
-    termcolor
-    # end of list
-
-export PATH="$PATH:/opt/ghc/bin:/opt/cabal/bin"
-pushd "$COGENT_DIR"
-    git submodule update --init --depth 1 --recursive -- isabelle
-    ln -s "$PWD/isabelle/bin/isabelle" /usr/local/bin/isabelle
-
-    isabelle components -I
-    isabelle components -a
-
-    wget "http://ts.data61.csiro.au/projects/TS/autocorres/${AC_VER}.tar.gz"
-    tar -xf "${AC_VER}.tar.gz" && rm "${AC_VER}.tar.gz"
-    mv "${AC_VER}" "${AC_DIR}"
-
-    pushd cogent
-        sed -i 's/^jobs:.*$/jobs: 2/' "$HOME/.cabal/config"
-        #cp misc/cabal.config.d/cabal.config-8.6.5 cabal.config
-
-        cabal v1-install --only-dependencies --force-reinstalls --enable-tests --dry -v --flags="haskell-backend docgent"
-        cabal v1-install --only-dependencies --force-reinstalls --flags="haskell-backend docgent";  # --enable-tests;
-        cabal v1-configure --flags="haskell-backend docgent"
-        cabal v1-install --force-reinstalls --flags="haskell-backend docgent"
-    popd
-popd
-
-# Isabelle downloads tar.gz files, and then uncompresses them for its contrib.
-# We don't need both the uncompressed AND decompressed versions, but Isabelle
-# checks for the tarballs. To fool it, we now truncate the tars and save disk space.
-pushd "$HOME/.isabelle/contrib"
-    truncate -s0 ./*.tar.gz
-    ls -lah  # show the evidence
-popd
-as_root rm -rf /tmp/isabelle-  # This is a random tmp folder isabelle makes