diff --git a/.forgejo/workflows/lean_action_ci.yml b/.forgejo/workflows/lean_action_ci.yml
new file mode 100644
index 0000000..a494136
--- /dev/null
+++ b/.forgejo/workflows/lean_action_ci.yml
@@ -0,0 +1,24 @@
+name: Lean Action CI
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v5
+
+      - name: Install Rust toolchain
+        uses: dtolnay/rust-toolchain@stable
+
+      - name: Build Rust cubical kernel
+        run: cd native/cubical && cargo build --release
+
+      - uses: leanprover/lean-action@v1
+
+      - name: Run cubical-test
+        run: ./.lake/build/bin/cubical-test
diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml
deleted file mode 100644
index c48bd68..0000000
--- a/.github/workflows/lean_action_ci.yml
+++ /dev/null
@@ -1,14 +0,0 @@
-name: Lean Action CI
-
-on:
-  push:
-  pull_request:
-  workflow_dispatch:
-
-jobs:
-  build:
-    runs-on: ubuntu-latest
-
-    steps:
-      - uses: actions/checkout@v5
-      - uses: leanprover/lean-action@v1
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..b92876f
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,27 @@
+Copyright (c) 2026 Maximus Gorog. All rights reserved.
+
+This software and the associated source files, documentation, build
+scripts, configuration, and other materials in this repository
+(collectively, the "Software") are the proprietary and confidential
+property of the copyright holder.
+
+NO LICENSE IS GRANTED.  The presence of this Software in a publicly
+accessible repository does not, by itself, grant any permission to
+use, copy, modify, merge, publish, distribute, sublicense, link
+against, embed, or create derivative works of the Software, in whole
+or in part, for any purpose.
+
+Use of any kind — including but not limited to compilation, execution,
+incorporation into other software, or redistribution in any form —
+requires express prior written consent from the copyright holder.
+Unauthorized use is prohibited.
+
+For licensing inquiries, contact: mgorog@gmail.com
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE, AND
+NONINFRINGEMENT.  IN NO EVENT SHALL THE COPYRIGHT HOLDER BE LIABLE
+FOR ANY CLAIM, DAMAGES, OR OTHER LIABILITY, WHETHER IN AN ACTION OF
+CONTRACT, TORT, OR OTHERWISE, ARISING FROM, OUT OF, OR IN CONNECTION
+WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
diff --git a/README.md b/README.md
index 5b21ac8..d212bfb 100644
--- a/README.md
+++ b/README.md
@@ -21,7 +21,12 @@ preserves the Lean-level proofs.
 - `CubicalTest.lean`, `CubicalBench.lean` — engine smoke + property
   tests (62/62 passing) and microbenchmarks.
 
-## Reusing this engine
+## Consuming the engine (with permission)
+
+This Software is **proprietary**.  See `LICENSE` — no use is granted
+by virtue of the repository being public.  The instructions below
+are for the copyright holder and any party with prior written consent
+from `mgorog@gmail.com`.
 
 Add as a Lake dependency from another Lean 4 project: