ci: Add GitHub Actions for Rust, Lean and Rocq

.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

.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: ''

.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

.gitignore

@@ -89,10 +89,6 @@ Temporary Items
 debug/
 target/
 
-# Remove Cargo.lock from gitignore if creating an executable, leave it for libraries
-# More information here https://doc.rust-lang.org/cargo/guide/cargo-toml-vs-cargo-lock.html
-Cargo.lock
-
 # These are backup files generated by rustfmt
 **/*.rs.bk
 

README.md

@@ -0,0 +1,45 @@
+# Einsof
+
+> Work in progress.
+
+Einsof is a security authorization system for LLM tool execution. It addresses the
+[Lethal Trifecta](https://simonwillison.net/2025/Jun/16/the-lethal-trifecta/) -- the
+combination of private data, untrusted content, and external communication that enables
+data exfiltration through indirect prompt injection.
+
+The system enforces authorization at tool boundaries so that a confused (prompt-injected)
+agent cannot reach egress channels when it carries taint from private data.
+
+## Components
+
+### [Tzimtzum](tzimtzum/) -- Formal Specification
+
+The TzimtzumV2 protocol, written in Lean 4 using the
+[Veil](https://github.com/verse-lab/veil) verification framework. All 7 safety properties
+and 12 strengthening invariants are verified automatically via push-button SMT
+
+### [Argus](argus/) -- Rust Implementation
+
+A tool authorization gateway implementing the TzimtzumV2 protocol. Rust workspace with
+10 crates covering the core state machine, policy engine, MCP server management, LLM proxy,
+gRPC API, sandboxing, and more. 512+ tests across the workspace.
+
+### [Formal Proofs](argus/formal/) -- Rocq (Coq) Verification
+
+Mechanized proofs connecting the Lean specification to the Rust implementation. Three layers:
+axioms (data structure interfaces), abstract specification (safety properties), and refinement
+proofs (simulation relations and soundness guarantees).
+
+## Toolchain
+
+Managed via [mise](https://mise.jdx.dev/):
+
+| Tool  | Version |
+|-------|---------|
+| Rust  | 1.93.0  |
+| Lean  | 4.27.0  |
+| Rocq  | 9.0     |
+
+## License
+
+MIT