From 5bf2f18b7a74c3495fb64d14dd7876eaad36a02f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?C=CE=BBstor?= <ygorcastor@gmail.com>
Date: Fri, 13 Mar 2026 15:20:06 +0100
Subject: [PATCH 1/4] ci: Add GitHub Actions for Rust, Lean and Rocq

---
 .github/workflows/lean.yml | 24 ++++++++++++++++++++++++
 .github/workflows/rocq.yml | 31 +++++++++++++++++++++++++++++++
 .github/workflows/rust.yml | 32 ++++++++++++++++++++++++++++++++
 3 files changed, 87 insertions(+)
 create mode 100644 .github/workflows/lean.yml
 create mode 100644 .github/workflows/rocq.yml
 create mode 100644 .github/workflows/rust.yml

diff --git a/.github/workflows/lean.yml b/.github/workflows/lean.yml
new file mode 100644
index 0000000..697c86c
--- /dev/null
+++ b/.github/workflows/lean.yml
@@ -0,0 +1,24 @@
+name: Lean Verification
+
+on:
+  push:
+    paths:
+      - 'tzimtzum/**'
+  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..b9ea037
--- /dev/null
+++ b/.github/workflows/rocq.yml
@@ -0,0 +1,31 @@
+name: Rocq Proofs
+
+on:
+  push:
+    paths:
+      - 'argus/formal/**'
+  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..9bcf4ef
--- /dev/null
+++ b/.github/workflows/rust.yml
@@ -0,0 +1,32 @@
+name: Rust CI
+
+on:
+  push:
+  pull_request:
+
+jobs:
+  rust-ci:
+    name: Build, Lint & Test
+    runs-on: ubuntu-latest
+    defaults:
+      run:
+        working-directory: argus
+    steps:
+      - uses: actions/checkout@v4
+
+      - uses: jdx/mise-action@v2
+
+      - 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

From d93ae051ec0d4a3a8bc438a3a91b6a9d0c8840a2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?C=CE=BBstor?= <ygorcastor@gmail.com>
Date: Fri, 13 Mar 2026 15:22:10 +0100
Subject: [PATCH 2/4] ci: Only run on pull requests

---
 .github/workflows/lean.yml | 3 ---
 .github/workflows/rocq.yml | 3 ---
 .github/workflows/rust.yml | 1 -
 3 files changed, 7 deletions(-)

diff --git a/.github/workflows/lean.yml b/.github/workflows/lean.yml
index 697c86c..caa53d1 100644
--- a/.github/workflows/lean.yml
+++ b/.github/workflows/lean.yml
@@ -1,9 +1,6 @@
 name: Lean Verification
 
 on:
-  push:
-    paths:
-      - 'tzimtzum/**'
   pull_request:
     paths:
       - 'tzimtzum/**'
diff --git a/.github/workflows/rocq.yml b/.github/workflows/rocq.yml
index b9ea037..cf4bf9b 100644
--- a/.github/workflows/rocq.yml
+++ b/.github/workflows/rocq.yml
@@ -1,9 +1,6 @@
 name: Rocq Proofs
 
 on:
-  push:
-    paths:
-      - 'argus/formal/**'
   pull_request:
     paths:
       - 'argus/formal/**'
diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml
index 9bcf4ef..56761ef 100644
--- a/.github/workflows/rust.yml
+++ b/.github/workflows/rust.yml
@@ -1,7 +1,6 @@
 name: Rust CI
 
 on:
-  push:
   pull_request:
 
 jobs:

From 55b353b3f444e11b661fbfa0ed634736a82f6eb7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?C=CE=BBstor?= <ygorcastor@gmail.com>
Date: Fri, 13 Mar 2026 15:22:43 +0100
Subject: [PATCH 3/4] ci: Add rustfmt and clippy components

---
 .github/workflows/rust.yml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml
index 56761ef..fe328c4 100644
--- a/.github/workflows/rust.yml
+++ b/.github/workflows/rust.yml
@@ -15,6 +15,9 @@ jobs:
 
       - uses: jdx/mise-action@v2
 
+      - name: Install Rust components
+        run: rustup component add rustfmt clippy
+
       - name: Check formatting
         run: cargo fmt --check
 

From e8f055bfa404cc4a947c84d0e7e0ee03f923d1be Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?C=CE=BBstor?= <ygorcastor@gmail.com>
Date: Fri, 13 Mar 2026 15:29:06 +0100
Subject: [PATCH 4/4] ci: Add protoc setup

---
 .github/workflows/rust.yml | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml
index fe328c4..41362a5 100644
--- a/.github/workflows/rust.yml
+++ b/.github/workflows/rust.yml
@@ -13,6 +13,10 @@ jobs:
     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