diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index c3fb38184..12143e2f3 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -11,6 +11,8 @@ jobs:
     runs-on: macos-latest
     steps:
       - uses: actions/checkout@v4
+      - name: install native dependencies
+        run: brew install litani
       - name: Setup nix
         uses: ./.github/actions/setup-nix
         with:
@@ -20,6 +22,7 @@ jobs:
               Architecture: $(uname -m)
               - $(nix --version)
               - $(astyle --version)
+              - $(cbmc --version)
               - $(${{ matrix.cross_prefix }}gcc --version | grep -m1 "")
               - $(bash --version | grep -m1 "")
             EOF
@@ -55,3 +58,10 @@ jobs:
             $(checksum ./test/gen_NISTKAT768  21b4a1e1ea34a13c26a9da5eeb9325afb5ca11596ca6f3704c3f2637e3ea7524)
             $(checksum ./test/gen_NISTKAT1024 6471398b0a728ee1ef39e93bb89b526fbf59587a3662edadbcfc6c88a512cd71)
           EOF
+      - name: Run CBMC proofs
+        shell: nix develop .#ci -c bash -e {0}
+        run: |
+          cd cbmc/proofs;
+          KYBER_K=2 ./run-cbmc-proofs.py --summarize;
+          KYBER_K=3 ./run-cbmc-proofs.py --summarize;
+          KYBER_K=4 ./run-cbmc-proofs.py --summarize;
diff --git a/flake.nix b/flake.nix
index 3e6928982..dff7fd10f 100644
--- a/flake.nix
+++ b/flake.nix
@@ -23,6 +23,7 @@
               inherit (pkgs)
                 # formatter & linters
                 astyle# 3.4.10
+                cbmc
                 nixpkgs-fmt
                 shfmt;
             }