diff --git a/.github/workflows/lean.yml b/.github/workflows/lean.yml
new file mode 100644
index 0000000..caa53d1
--- /dev/null
+++ b/.github/workflows/lean.yml
@@ -0,0 +1,21 @@
+name: Lean Verification
+
+on:
+  pull_request:
+    paths:
+      - 'tzimtzum/**'
+
+jobs:
+  lean-verify:
+    name: Verify TzimtzumV2
+    runs-on: ubuntu-latest
+    defaults:
+      run:
+        working-directory: tzimtzum
+    steps:
+      - uses: actions/checkout@v4
+
+      - uses: jdx/mise-action@v2
+
+      - name: Build and verify
+        run: make build
diff --git a/.github/workflows/rocq.yml b/.github/workflows/rocq.yml
new file mode 100644
index 0000000..cf4bf9b
--- /dev/null
+++ b/.github/workflows/rocq.yml
@@ -0,0 +1,28 @@
+name: Rocq Proofs
+
+on:
+  pull_request:
+    paths:
+      - 'argus/formal/**'
+
+jobs:
+  rocq-proofs:
+    name: Verify Formal Proofs
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - uses: coq-community/docker-coq-action@v1
+        with:
+          custom_image: 'rocq/rocq-prover:9.0'
+          before_script: |
+            startGroup "Fix permissions"
+              sudo chown -R 1000:1000 .
+            endGroup
+          script: |
+            startGroup "Build proofs"
+              cd argus/formal
+              coq_makefile -f _CoqProject -o Makefile.coq
+              make -f Makefile.coq -j2
+            endGroup
+          uninstall: ''
diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml
new file mode 100644
index 0000000..41362a5
--- /dev/null
+++ b/.github/workflows/rust.yml
@@ -0,0 +1,38 @@
+name: Rust CI
+
+on:
+  pull_request:
+
+jobs:
+  rust-ci:
+    name: Build, Lint & Test
+    runs-on: ubuntu-latest
+    defaults:
+      run:
+        working-directory: argus
+    steps:
+      - uses: actions/checkout@v4
+
+      - uses: arduino/setup-protoc@v3
+        with:
+          repo-token: ${{ secrets.GITHUB_TOKEN }}
+
+      - uses: jdx/mise-action@v2
+
+      - name: Install Rust components
+        run: rustup component add rustfmt clippy
+
+      - name: Check formatting
+        run: cargo fmt --check
+
+      - name: Clippy
+        run: cargo clippy --workspace -- -D warnings
+
+      - name: Run tests
+        run: cargo test --workspace
+
+      - name: Install cargo-audit
+        run: cargo install cargo-audit --locked
+
+      - name: Security audit
+        run: cargo audit