diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
new file mode 100644
index 000000000..30404c9ac
--- /dev/null
+++ b/.github/workflows/ci.yml
@@ -0,0 +1,139 @@
+name: CI
+on:
+  push:
+    branches-ignore:
+    - _**
+  pull_request:
+  merge_group:
+  workflow_dispatch:
+
+defaults:
+  run:
+    shell: bash
+
+jobs:
+  ci:
+    runs-on: ubuntu-latest
+    container: mtzguido/dev-base
+    steps:
+      - name: Cleanup
+        run: sudo find . -delete
+
+      - run: echo "HOME=/home/user" | sudo tee -a $GITHUB_ENV
+      - uses: mtzguido/set-opam-env@master
+      - run: opam install -y hex re ctypes sha sexplib
+      # ^ not in base
+
+      - uses: actions/checkout@master
+        id: checkout-fstar
+        with:
+          path: FStar
+          repository: FStarLang/FStar
+          ref: master
+
+      - name: Try fetch built F*
+        id: cache-fstar
+        uses: actions/cache/restore@v4
+        with:
+          path: FStar
+          key: FStar-${{ runner.os }}-${{ runner.arch }}-${{ steps.checkout-fstar.outputs.commit }}
+
+      - name: Build F*
+        if: steps.cache-fstar.outputs.cache-hit != 'true'
+        run: |
+          make -C FStar -sj$(nproc) ADMIT=1
+
+      - name: Save built F*
+        if: steps.cache-fstar.outputs.cache-hit != 'true'
+        uses: actions/cache/save@v4
+        with:
+          path: FStar
+          key: FStar-${{ runner.os }}-${{ runner.arch }}-${{ steps.checkout-fstar.outputs.commit }}
+
+      - run: echo "FSTAR_HOME=$(pwd)/FStar" | sudo tee -a $GITHUB_ENV
+      - run: echo "FSTAR_EXE=$(pwd)/FStar/bin/fstar.exe" | sudo tee -a $GITHUB_ENV
+      - run: echo "$(pwd)/FStar/bin" | sudo tee -a $GITHUB_PATH
+      # FSTAR_HOME just for compat. *Either* of the other two should suffice, eventually.
+
+      - uses: actions/checkout@master
+        id: checkout-karamel
+        with:
+          path: karamel
+          repository: FStarLang/karamel
+          ref: master
+
+      - name: Try fetch built karamel
+        id: cache-karamel
+        uses: actions/cache/restore@v4
+        with:
+          path: karamel
+          key: karamel-${{ runner.os }}-${{ runner.arch }}-${{ steps.checkout-fstar.outputs.commit }}-${{ steps.checkout-karamel.outputs.commit }}
+
+      - name: Build karamel (if not cached)
+        if: steps.cache-karamel.outputs.cache-hit != 'true'
+        run: |
+          make -C karamel -sj$(nproc) ADMIT=1
+
+      - name: Save built karamel
+        if: steps.cache-karamel.outputs.cache-hit != 'true'
+        uses: actions/cache/save@v4
+        with:
+          path: karamel
+          key: karamel-${{ runner.os }}-${{ runner.arch }}-${{ steps.checkout-fstar.outputs.commit }}-${{ steps.checkout-karamel.outputs.commit }}
+
+      - run: echo "KRML_HOME=$(pwd)/karamel" | sudo tee -a $GITHUB_ENV
+      - run: echo "KRML_EXE=$(pwd)/karamel/krml" | sudo tee -a $GITHUB_ENV
+      - run: echo "$(pwd)/karamel" | sudo tee -a $GITHUB_PATH
+
+      - uses: actions/checkout@master
+        with:
+          path: everparse
+
+      - name: Everparse CI
+        id: cistep
+        run: make -C everparse ci -skj$(nproc)
+
+      # I'm leaving this disabled as I do not get good incrementality
+      # when trying this out by hand due to dependence hash mismatches
+      # everywhere.
+      - name: Incrementality test
+        if: false
+        working-directory: everparse/tests/sample
+        run: |
+            echo 'let foo : FStar.UInt32.t = 42ul' >> Data.fsti
+            echo 'let foo : FStar.UInt32.t = Data.foo' >> Test.fst
+            make -j$(nproc)
+            git checkout Test.fst
+            sed -i 's!payloads!payload!g' Test.rfc
+            make -j$(nproc)
+            git checkout Test.rfc
+
+      - name: Calculate Time
+        if: ${{ always () }}
+        id: duration
+        uses: RockyIsHere/actions-calculate-log-time@v0.2.4
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+
+      - name: Post result to Zulip
+        if: ${{ always () }} # && secrets.ZULIP_API_KEY != '' }}
+        continue-on-error: true
+        uses: zulip/github-actions-zulip/send-message@v1
+        with:
+          api-key: ${{ secrets.ZULIP_API_KEY }}
+          email: "github-commits-bot@fstar.zulipchat.com"
+          organization-url: "https://fstar.zulipchat.com"
+          to: "everparse-ci"
+          type: "stream"
+          topic: "CI on '${{github.ref_name}}'"
+          content: |
+            '${{ github.event.head_commit.message || github.event.pull_request.title || github.head_commit.message }}' by ${{ github.event.head_commit.author.username || github.event.pull_request.user.login || github.head_commit.author.username }} (commit [${{github.sha}}](${{ github.event.head_commit.url || github.even.pull_request.html_url}}))
+            Status: ${{ steps.cistep.outcome == 'success' && '✅' || steps.cistep.outcome == 'cancelled' && '⚠' || '❌' }} ([link](https://github.com/${{github.repository}}/actions/runs/${{github.run_id}}))
+            Elapsed time: ${{ steps.duration.outputs.duration }}
+
+  # No-op job for branch protection.
+  ciok:
+    runs-on: ubuntu-latest
+    needs: ci
+    steps:
+      - run: exit 0