diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
new file mode 100644
index 0000000..85249d7
--- /dev/null
+++ b/.github/workflows/ci.yml
@@ -0,0 +1,45 @@
+on:
+  push:
+  pull_request:
+
+name: Continuous Integration
+
+jobs:
+  build:
+    strategy:
+      matrix:
+        toolchain:
+          - "leanprover/lean4:4.5.0"
+          - "leanprover/lean4:4.6.0-rc1"
+    name: Build and test
+    runs-on: ubuntu-latest
+    steps:
+      - name: Install elan
+        run: |
+          set -o pipefail
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          ./elan-init -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+      - uses: actions/checkout@v3
+
+      - name: List all files
+        run: |
+          find . -name "*.lean" -type f
+
+      - name: Select Lean version
+        run: |
+          echo "${{ matrix.toolchain }}" > lean-toolchain
+
+      - name: Lean version
+        run: |
+          lean --version
+
+      - name: Cache .lake
+        uses: actions/cache@v3
+        with:
+          path: .lake
+          key: ${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('lean-toolchain') }}
+          
+      - name: Build the project
+        run: |
+          lake build
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..1824d0c
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,3 @@
+/build
+/lakefile.olean
+/lake-packages/*
diff --git a/Main.lean b/Main.lean
new file mode 100644
index 0000000..adaf709
--- /dev/null
+++ b/Main.lean
@@ -0,0 +1,4 @@
+import «Subverso»
+
+def main : IO Unit :=
+  IO.println s!"Hello, {hello}!"
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..e6bb607
--- /dev/null
+++ b/README.md
@@ -0,0 +1,9 @@
+# Subverso - Verso's Library for Subprocesses
+
+Subverso is a support library that allows a
+[Verso](https://github.com/leanprover/verso) document to describe Lean
+code written in multiple versions of Lean. Verso itself may be tied to
+new Lean versions, because it makes use of new compiler features. This
+library will maintain broader compatibility with various Lean versions.
+
+
diff --git a/Subverso.lean b/Subverso.lean
new file mode 100644
index 0000000..caaa2dd
--- /dev/null
+++ b/Subverso.lean
@@ -0,0 +1,3 @@
+-- This module serves as the root of the `Subverso` library.
+-- Import modules here that should be built as part of the library.
+import «Subverso».Basic
\ No newline at end of file
diff --git a/Subverso/Basic.lean b/Subverso/Basic.lean
new file mode 100644
index 0000000..e99d3a6
--- /dev/null
+++ b/Subverso/Basic.lean
@@ -0,0 +1 @@
+def hello := "world"
\ No newline at end of file
diff --git a/lakefile.lean b/lakefile.lean
new file mode 100644
index 0000000..e989c93
--- /dev/null
+++ b/lakefile.lean
@@ -0,0 +1,16 @@
+import Lake
+open Lake DSL
+
+package «subverso» where
+  -- add package configuration options here
+
+lean_lib «Subverso» where
+  -- add library configuration options here
+
+@[default_target]
+lean_exe «subverso» where
+  root := `Main
+  -- Enables the use of the Lean interpreter by the executable (e.g.,
+  -- `runFrontend`) at the expense of increased binary size on Linux.
+  -- Remove this line if you do not need such functionality.
+  supportInterpreter := true
diff --git a/lean-toolchain b/lean-toolchain
new file mode 100644
index 0000000..2bf5ad0
--- /dev/null
+++ b/lean-toolchain
@@ -0,0 +1 @@
+stable