diff --git a/.github/workflows/prusti.yml b/.github/workflows/prusti.yml
new file mode 100644
index 0000000..56c9f32
--- /dev/null
+++ b/.github/workflows/prusti.yml
@@ -0,0 +1,38 @@
+# This Source Code Form is subject to the terms of the Mozilla Public
+# License, v. 2.0. If a copy of the MPL was not distributed with this
+# file, You can obtain one at http://mozilla.org/MPL/2.0/.
+#
+# Copyright (c) 2022 ETH Zurich.
+
+name: Verify and Lint
+
+on:
+  push:
+  branches:
+    - main
+  pull_request: # run this workflow on every pull_request
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout the current repository
+        uses: actions/checkout@v3
+      - name: Verify the examples and exercises written in Prusti
+        uses: viperproject/prusti-action@v1
+        with:
+          path: '.'
+
+  clippy_check:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v3
+      - uses: actions-rs/toolchain@v1
+        with:
+            toolchain: nightly
+            components: clippy
+            override: true
+      - uses: actions-rs/clippy-check@v1
+        with:
+          token: ${{ secrets.GITHUB_TOKEN }}
+          args: --manifest-path Cargo.toml --all-features -- -D warnings
diff --git a/Cargo.lock b/Cargo.lock
new file mode 100644
index 0000000..bab9ffb
--- /dev/null
+++ b/Cargo.lock
@@ -0,0 +1,133 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 3
+
+[[package]]
+name = "cfg-if"
+version = "1.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
+
+[[package]]
+name = "chapter1"
+version = "0.1.0"
+dependencies = [
+ "prusti-contracts",
+]
+
+[[package]]
+name = "chapter2"
+version = "0.1.0"
+dependencies = [
+ "prusti-contracts",
+]
+
+[[package]]
+name = "chapter3"
+version = "0.1.0"
+dependencies = [
+ "prusti-contracts",
+ "rand",
+]
+
+[[package]]
+name = "chapter4"
+version = "0.1.0"
+dependencies = [
+ "prusti-contracts",
+]
+
+[[package]]
+name = "chapter5"
+version = "0.1.0"
+dependencies = [
+ "prusti-contracts",
+]
+
+[[package]]
+name = "chapter8"
+version = "0.1.0"
+dependencies = [
+ "prusti-contracts",
+]
+
+[[package]]
+name = "chapter9"
+version = "0.1.0"
+dependencies = [
+ "prusti-contracts",
+]
+
+[[package]]
+name = "getrandom"
+version = "0.2.8"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c05aeb6a22b8f62540c194aac980f2115af067bfe15a0734d7277a768d396b31"
+dependencies = [
+ "cfg-if",
+ "libc",
+ "wasi",
+]
+
+[[package]]
+name = "libc"
+version = "0.2.139"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "201de327520df007757c1f0adce6e827fe8562fbc28bfd9c15571c66ca1f5f79"
+
+[[package]]
+name = "ppv-lite86"
+version = "0.2.17"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5b40af805b3121feab8a3c29f04d8ad262fa8e0561883e7653e024ae4479e6de"
+
+[[package]]
+name = "prusti-contracts"
+version = "0.1.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0a55ba828aceca3c0786a6dd252e1d219720d15f4c454b70fee282111469c940"
+dependencies = [
+ "prusti-contracts-proc-macros",
+]
+
+[[package]]
+name = "prusti-contracts-proc-macros"
+version = "0.1.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b74f012498f2f2239b7c99cb07c6fd18271587163d1710a242f00b6af5d9043d"
+
+[[package]]
+name = "rand"
+version = "0.8.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "34af8d1a0e25924bc5b7c43c079c942339d8f0a8b57c39049bef581b46327404"
+dependencies = [
+ "libc",
+ "rand_chacha",
+ "rand_core",
+]
+
+[[package]]
+name = "rand_chacha"
+version = "0.3.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e6c10a63a0fa32252be49d21e7709d4d4baf8d231c2dbce1eaa8141b9b127d88"
+dependencies = [
+ "ppv-lite86",
+ "rand_core",
+]
+
+[[package]]
+name = "rand_core"
+version = "0.6.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ec0be4795e2f6a28069bec0b5ff3e2ac9bafc99e6a9a7dc3547996c5c816922c"
+dependencies = [
+ "getrandom",
+]
+
+[[package]]
+name = "wasi"
+version = "0.11.0+wasi-snapshot-preview1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423"
diff --git a/Cargo.toml b/Cargo.toml
new file mode 100644
index 0000000..8fae341
--- /dev/null
+++ b/Cargo.toml
@@ -0,0 +1,3 @@
+[workspace]
+members = ["chapter*"]
+exclude = ["lists"]
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..3872f23
--- /dev/null
+++ b/README.md
@@ -0,0 +1,47 @@
+# `program-proofs-prusti`
+
+Examples and exercises from the book [*Program Proofs*](https://program-proofs.com/) by K. Rustan M. Leino translated to Rust and verified with [Prusti](https://prusti.ethz.ch/), a deductive verifier for Rust programs developed at ETH Zurich.
+
+## Repository structure
+
+Each chapter of the book that we have translated can be found in its own crate at the root of this repository.
+
+Each crate can be verified, as a whole, using [`cargo prusti`](https://viperproject.github.io/prusti-dev/user-guide/basic.html#command-line) from the command line or using the [Prusti Assistant](https://viperproject.github.io/prusti-dev/user-guide/basic.html#prusti-assistant) extension for VS Code.
+
+Within each crate, there are two main subdirectories of interest:
+
+- `(chapter)/src/examples` - contains translated *examples*, i.e. various snippets of code from the given chapter;
+- `(chapter)/src/exercises` - contains translated *exercises*, i.e. (possible) solutions to the exercises from the given chapter.
+
+Files in these subdirectories follow the naming scheme `example_(section)_(subsection).rs` or `exercise_(section)_(subsection).rs`. The remaining files in each crate serve to configure Prusti, configure Cargo, and to tie together the example and exercise files.
+
+## Current status
+
+|            | Chapter | Notes |
+| ----------:| ------- | ----- |
+| **PART 0** | **Learning the Ropes** | |
+| Chapter 1  | [Basics](chapter1) | |
+| Chapter 2  | [Making it Formal](chapter2) | |
+| Chapter 3  | [Recursion and Termination](chapter3) | Termination checking is not yet supported in Prusti |
+| Chapter 4  | [Inductive Datatypes](chapter4) | |
+| Chapter 5  | [Lemmas and Proofs](chapter5) | Ghost code is not yet supported in Prusti |
+| **PART 1** | **Functional Programs** | |
+| Chapter 6  | ~~Lists~~ | (Skipped) |
+| Chapter 7  | ~~Unary Numbers~~ | (Skipped) |
+| Chapter 8  | [Sorting](chapter8) | |
+| Chapter 9  | [Modules](chapter9) | |
+| Chapter 10 | ~~Data-Structure Invariants~~ | (Skipped) |
+| **PART 2** | **Imperative Programs** | |
+| Chapter 11 | ~~Loops~~ | (Skipped) |
+| Chapter 12 | ~~Recursive Specifications, Iterative Programs~~ | (Skipped) |
+| Chapter 13 | ~~Arrays and Searching~~ | (Skipped) |
+| Chapter 14 | [Modifying Arrays](chapter14) | |
+| Chapter 15 | ~~In-situ Sorting~~ | (Skipped) | |
+| Chapter 16 | [Objects](chapter16) | |
+| Chapter 17 | [Mutable Data Structures](chapter17) | |
+
+## References
+
+The translations found in this repository were developed as part of Patrick Muntwiler's BSc thesis.
+
+- Muntwiler, Patrick. ["Evaluating and Documenting a Rust Verifier."](https://ethz.ch/content/dam/ethz/special-interest/infk/chair-program-method/pm/documents/Education/Theses/Patrick_Muntwiler_BS_Thesis.pdf) (2023).