diff --git a/.github/ci.sh b/.github/ci.sh
new file mode 100755
index 0000000..fbe8920
--- /dev/null
+++ b/.github/ci.sh
@@ -0,0 +1,43 @@
+#!/usr/bin/env bash
+set -Eeuxo pipefail
+
+DATE=$(date "+%Y-%m-%d")
+[[ "$RUNNER_OS" == 'Windows' ]] && IS_WIN=true || IS_WIN=false
+BIN=bin
+EXT=""
+$IS_WIN && EXT=".exe"
+mkdir -p "$BIN"
+
+is_exe() { [[ -x "$1/$2$EXT" ]] || command -v "$2" > /dev/null 2>&1; }
+
+install_llvm() {
+  if [[ "$RUNNER_OS" = "Linux" ]]; then
+    sudo apt-get update -q && sudo apt-get install -y clang-$LLVM_VERSION llvm-$LLVM_VERSION-tools
+  else
+    echo "$RUNNER_OS is not currently supported."
+    return 1
+  fi
+  echo "CLANG=clang-$LLVM_VERSION" >> "$GITHUB_ENV"
+  echo "LLVM_AS=llvm-as-$LLVM_VERSION" >> "$GITHUB_ENV"
+  echo "LLVM_LINK=llvm-link-$LLVM_VERSION" >> "$GITHUB_ENV"
+}
+
+install_solvers() {
+  (cd $BIN && curl -o bins.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/$SOLVER_PKG_VERSION/$BUILD_TARGET_OS-bin.zip" && unzip -o bins.zip && rm bins.zip)
+  cp $BIN/yices_smt2$EXT $BIN/yices-smt2$EXT
+  chmod +x $BIN/*
+}
+
+install_system_deps() {
+  install_solvers
+  install_llvm
+  # wait
+  export PATH=$PWD/$BIN:$PATH
+  echo "$PWD/$BIN" >> $GITHUB_PATH
+  is_exe "$BIN" z3 && is_exe "$BIN" cvc4 && is_exe "$BIN" cvc5 && is_exe "$BIN" yices
+}
+
+COMMAND="$1"
+shift
+
+"$COMMAND" "$@"
diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml
new file mode 100644
index 0000000..4e4752d
--- /dev/null
+++ b/.github/workflows/ci.yaml
@@ -0,0 +1,83 @@
+name: copilot-verifier
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+
+env:
+  SOLVER_PKG_VERSION: "snapshot-20221212"
+  # The CACHE_VERSION can be updated to force the use of a new cache if
+  # the current cache contents become corrupted/invalid.  This can
+  # sometimes happen when (for example) the OS version is changed but
+  # older .so files are cached, which can have various effects
+  # (e.g. cabal complains it can't find a valid version of the "happy"
+  # tool).
+  CACHE_VERSION: 1
+  LLVM_VERSION: 12
+
+jobs:
+  build:
+    runs-on: ${{ matrix.os }}
+    strategy:
+      fail-fast: false
+      matrix:
+        os: [ubuntu-22.04]
+        ghc-version: ["8.10.7", "9.0.2", "9.2.7"]
+        cabal: [ '3.8.1.0' ]
+    steps:
+      - uses: actions/checkout@v2
+        with:
+          submodules: true
+
+      - uses: haskell/actions/setup@v1
+        id: setup-haskell
+        with:
+          ghc-version: ${{ matrix.ghc-version }}
+          cabal-version: ${{ matrix.cabal }}
+
+      - uses: actions/cache/restore@v3
+        name: Restore cabal store cache
+        with:
+          path: |
+            ${{ steps.setup-haskell.outputs.cabal-store }}
+            dist-newstyle
+          key: ${{ env.CACHE_VERSION }}-cabal-${{ matrix.os }}-${{ matrix.ghc-version }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc-version)) }}-${{ github.sha }}
+          restore-keys: |
+            ${{ env.CACHE_VERSION }}-cabal-${{ matrix.os }}-${{ matrix.ghc-version }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc-version)) }}-
+
+      - shell: bash
+        name: Install system dependencies
+        run: .github/ci.sh install_system_deps
+        env:
+          BIN_ZIP_FILE: ${{ matrix.os }}-bin.zip
+          BUILD_TARGET_OS: ${{ matrix.os }}
+
+      - shell: bash
+        name: Update
+        run: cabal update
+
+      - shell: bash
+        name: Configure
+        run: cabal configure --enable-tests -j2 all
+
+      - shell: bash
+        name: Build copilot-verifier
+        run: cabal build pkg:copilot-verifier
+
+      - shell: bash
+        name: Build copilot-verifier-demo
+        run: cabal build pkg:copilot-verifier-demo
+
+      - shell: bash
+        name: Test copilot-verifier
+        run: cabal test pkg:copilot-verifier
+
+      - uses: actions/cache/save@v3
+        name: Save cabal store cache
+        if: always()
+        with:
+          path: |
+            ${{ steps.setup-haskell.outputs.cabal-store }}
+            dist-newstyle
+          key: ${{ env.CACHE_VERSION }}-cabal-${{ matrix.os }}-${{ matrix.ghc-version }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc-version)) }}-${{ github.sha }}