diff --git a/.github/workflows/build-userdocs.yml b/.github/workflows/build-userdocs.yml
new file mode 100644
index 000000000..57078e991
--- /dev/null
+++ b/.github/workflows/build-userdocs.yml
@@ -0,0 +1,12 @@
+name: Build Aeneas user docs and test them
+on: [push, pull_request]
+
+jobs:
+  test:
+    name: Test Aeneas user docs
+    runs-on: [self-hosted, linux, nix]
+    steps:
+    - uses: actions/checkout@v4
+    - name: Build the book
+      run: nix build '.?dir=docs/user'#book
+    # TODO: test the Lean examples code via nix build '.?dir=docs/user'#test or something similar.
diff --git a/.github/workflows/deploy-userdocs.yml b/.github/workflows/deploy-userdocs.yml
new file mode 100644
index 000000000..88f6b57cf
--- /dev/null
+++ b/.github/workflows/deploy-userdocs.yml
@@ -0,0 +1,32 @@
+name: Deploy Aeneas user docs to GitHub pages
+on:
+  push:
+    branches:
+      - main
+
+jobs:
+  deploy:
+    runs-on: [self-hosted, linux, nix]
+    permissions:
+      contents: write  # To push a branch
+      pull-requests: write  # To create a PR from that branch
+    steps:
+    - uses: actions/checkout@v4
+      with:
+        fetch-depth: 0
+    - name: Deploy GitHub Pages
+      run: |
+        # This assumes your book is in the root of your repository.
+        # Just add a `cd` here if you need to change to another directory.
+        nix build '.?dir=docs/user'#book -o html
+        git worktree add gh-pages
+        git config user.name "Deploy from CI"
+        git config user.email ""
+        cd gh-pages
+        # Delete the ref to avoid keeping history.
+        git update-ref -d refs/heads/gh-pages
+        rm -rf *
+        cp --dereference -vr ../html/* .
+        git add .
+        git commit -m "Deploy $GITHUB_SHA to gh-pages"
+        git push --force --set-upstream origin gh-pages
diff --git a/docs/user/.envrc b/docs/user/.envrc
new file mode 100644
index 000000000..3550a30f2
--- /dev/null
+++ b/docs/user/.envrc
@@ -0,0 +1 @@
+use flake
diff --git a/docs/user/.gitignore b/docs/user/.gitignore
new file mode 100644
index 000000000..7585238ef
--- /dev/null
+++ b/docs/user/.gitignore
@@ -0,0 +1 @@
+book
diff --git a/docs/user/book.toml b/docs/user/book.toml
new file mode 100644
index 000000000..333659cba
--- /dev/null
+++ b/docs/user/book.toml
@@ -0,0 +1,6 @@
+[book]
+authors = ["The Aeneas contributors"]
+language = "en"
+multilingual = false
+src = "src"
+title = "Aeneas user documentation"
diff --git a/docs/user/flake.lock b/docs/user/flake.lock
new file mode 100644
index 000000000..dfd3938b6
--- /dev/null
+++ b/docs/user/flake.lock
@@ -0,0 +1,256 @@
+{
+  "nodes": {
+    "alectryon": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1654613606,
+        "narHash": "sha256-IGCn1PzTyw8rrwmyWUiw3Jo/dyZVGkMslnHYW7YB8yk=",
+        "owner": "Kha",
+        "repo": "alectryon",
+        "rev": "c3b16f650665745e1da4ddfcc048d3bd639f71d5",
+        "type": "github"
+      },
+      "original": {
+        "owner": "Kha",
+        "ref": "typeid",
+        "repo": "alectryon",
+        "type": "github"
+      }
+    },
+    "flake-compat": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1673956053,
+        "narHash": "sha256-4gtG9iQuiKITOjNQQeQIpoIB6b16fm+504Ch3sNKLd8=",
+        "owner": "edolstra",
+        "repo": "flake-compat",
+        "rev": "35bb57c0c8d8b62bbfd284272c928ceb64ddbde9",
+        "type": "github"
+      },
+      "original": {
+        "owner": "edolstra",
+        "repo": "flake-compat",
+        "type": "github"
+      }
+    },
+    "flake-utils": {
+      "inputs": {
+        "systems": "systems"
+      },
+      "locked": {
+        "lastModified": 1710146030,
+        "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "lean": {
+      "inputs": {
+        "flake-utils": "flake-utils",
+        "lean4-mode": "lean4-mode",
+        "nix": "nix",
+        "nixpkgs": "nixpkgs_2",
+        "nixpkgs-old": "nixpkgs-old"
+      },
+      "locked": {
+        "lastModified": 1720529829,
+        "narHash": "sha256-hPqn4qRfe7bLAaNRvK1RDC50IUuCaxDCcv5NtNsETEQ=",
+        "owner": "leanprover",
+        "repo": "lean4",
+        "rev": "f531f4e5db8f402a015a69373af9a002fe754acd",
+        "type": "github"
+      },
+      "original": {
+        "owner": "leanprover",
+        "repo": "lean4",
+        "type": "github"
+      }
+    },
+    "lean4-mode": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1709737301,
+        "narHash": "sha256-uT9JN2kLNKJK9c/S/WxLjiHmwijq49EgLb+gJUSDpz0=",
+        "owner": "leanprover",
+        "repo": "lean4-mode",
+        "rev": "f1f24c15134dee3754b82c9d9924866fe6bc6b9f",
+        "type": "github"
+      },
+      "original": {
+        "owner": "leanprover",
+        "repo": "lean4-mode",
+        "type": "github"
+      }
+    },
+    "leanInk": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1706870309,
+        "narHash": "sha256-5HhF/0mmPVvmcScE4t/UTB6IPuf050UJhNZprEQZ/aw=",
+        "owner": "leanprover",
+        "repo": "LeanInk",
+        "rev": "c54475dffc030aa67113eff600105b62eca646db",
+        "type": "github"
+      },
+      "original": {
+        "owner": "leanprover",
+        "repo": "LeanInk",
+        "type": "github"
+      }
+    },
+    "libgit2": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1697646580,
+        "narHash": "sha256-oX4Z3S9WtJlwvj0uH9HlYcWv+x1hqp8mhXl7HsLu2f0=",
+        "owner": "libgit2",
+        "repo": "libgit2",
+        "rev": "45fd9ed7ae1a9b74b957ef4f337bc3c8b3df01b5",
+        "type": "github"
+      },
+      "original": {
+        "owner": "libgit2",
+        "repo": "libgit2",
+        "type": "github"
+      }
+    },
+    "mdBook": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1660074464,
+        "narHash": "sha256-W30G7AeWBjdJE/CQZJU5vJjaDGZtpmxEKNMEvaYtuF8=",
+        "owner": "leanprover",
+        "repo": "mdBook",
+        "rev": "9321c10c502cd59eea8afc4325a84eab3ddf9391",
+        "type": "github"
+      },
+      "original": {
+        "owner": "leanprover",
+        "repo": "mdBook",
+        "type": "github"
+      }
+    },
+    "nix": {
+      "inputs": {
+        "flake-compat": "flake-compat",
+        "libgit2": "libgit2",
+        "nixpkgs": "nixpkgs",
+        "nixpkgs-regression": "nixpkgs-regression"
+      },
+      "locked": {
+        "lastModified": 1711102798,
+        "narHash": "sha256-CXOIJr8byjolqG7eqCLa+Wfi7rah62VmLoqSXENaZnw=",
+        "owner": "NixOS",
+        "repo": "nix",
+        "rev": "a22328066416650471c3545b0b138669ea212ab4",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "repo": "nix",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1709083642,
+        "narHash": "sha256-7kkJQd4rZ+vFrzWu8sTRtta5D1kBG0LSRYAfhtmMlSo=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "b550fe4b4776908ac2a861124307045f8e717c8e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "release-23.11",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "nixpkgs-old": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1581379743,
+        "narHash": "sha256-i1XCn9rKuLjvCdu2UeXKzGLF6IuQePQKFt4hEKRU5oc=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "34c7eb7545d155cc5b6f499b23a7cb1c96ab4d59",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "nixos-19.03",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "nixpkgs-regression": {
+      "locked": {
+        "lastModified": 1643052045,
+        "narHash": "sha256-uGJ0VXIhWKGXxkeNnq4TvV3CIOkUJ3PAoLZ3HMzNVMw=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
+        "type": "github"
+      }
+    },
+    "nixpkgs_2": {
+      "locked": {
+        "lastModified": 1710889954,
+        "narHash": "sha256-Pr6F5Pmd7JnNEMHHmspZ0qVqIBVxyZ13ik1pJtm2QXk=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "7872526e9c5332274ea5932a0c3270d6e4724f3b",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "nixpkgs-unstable",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "alectryon": "alectryon",
+        "flake-utils": [
+          "lean",
+          "flake-utils"
+        ],
+        "lean": "lean",
+        "leanInk": "leanInk",
+        "mdBook": "mdBook"
+      }
+    },
+    "systems": {
+      "locked": {
+        "lastModified": 1681028828,
+        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+        "owner": "nix-systems",
+        "repo": "default",
+        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-systems",
+        "repo": "default",
+        "type": "github"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}
diff --git a/docs/user/flake.nix b/docs/user/flake.nix
new file mode 100644
index 000000000..be1576145
--- /dev/null
+++ b/docs/user/flake.nix
@@ -0,0 +1,110 @@
+# Taken from Lean documentation's flake.nix
+{
+  description = "Aeneas documentation";
+
+  inputs.lean.url = "github:leanprover/lean4";
+  inputs.flake-utils.follows = "lean/flake-utils";
+  inputs.mdBook = {
+    url = "github:leanprover/mdBook";
+    flake = false;
+  };
+  inputs.alectryon = {
+    url = "github:Kha/alectryon/typeid";
+    flake = false;
+  };
+  inputs.leanInk = {
+    url = "github:leanprover/LeanInk";
+    flake = false;
+  };
+
+  outputs = inputs@{ self, ... }: inputs.flake-utils.lib.eachDefaultSystem (system:
+    with inputs.lean.packages.${system}; with nixpkgs;
+    let
+      doc-src = ./.; # lib.sourceByRegex ../. ["doc.*" "tests(/lean(/beginEndAsMacro.lean)?)?"];
+    in {
+    packages = rec {
+      lean-mdbook = mdbook.overrideAttrs (drv: rec {
+        name = "lean-${mdbook.name}";
+        src = inputs.mdBook;
+        cargoDeps = drv.cargoDeps.overrideAttrs (_: {
+          inherit src;
+          outputHash = "sha256-CO3A9Kpp4sIvkT9X3p+GTidazk7Fn4jf0AP2PINN44A=";
+        });
+        doCheck = false;
+      });
+      book = stdenv.mkDerivation {
+        name = "aeneas-doc";
+        src = doc-src;
+        buildInputs = [ lean-mdbook ];
+        buildCommand = ''
+          mkdir $out
+          # necessary for `additional-css`...?
+          cp -vr --no-preserve=mode $src/* .
+          mdbook build -d $out
+        '';
+      };
+      # We use a separate derivation instead of `checkPhase` so we can push it but not `doc` to the binary cache
+      test = stdenv.mkDerivation {
+        name = "aeneas-doc-test";
+        src = doc-src;
+        buildInputs = [ lean-mdbook stage1.Lean.lean-package strace ];
+        patchPhase = ''
+          cd doc
+          patchShebangs test
+        '';
+        buildPhase = ''
+          mdbook test
+          touch $out
+        '';
+        dontInstall = true;
+      };
+
+      leanInk = (buildLeanPackage {
+        name = "Main";
+        src = inputs.leanInk;
+        deps = [ (buildLeanPackage {
+          name = "LeanInk";
+          src = inputs.leanInk;
+        }) ];
+        executableName = "leanInk";
+        linkFlags = ["-rdynamic"];
+      }).executable;
+
+      alectryon = python3Packages.buildPythonApplication {
+        name = "alectryon";
+        src = inputs.alectryon;
+        propagatedBuildInputs =
+          [ leanInk lean-all ] ++
+          # https://github.com/cpitclaudel/alectryon/blob/master/setup.cfg
+          (with python3Packages; [ pygments dominate beautifulsoup4 docutils ]);
+        doCheck = false;
+      };
+
+      renderLeanMod = mod: mod.overrideAttrs (final: prev: {
+        name = "${prev.name}.md";
+        buildInputs = prev.buildInputs ++ [ alectryon ];
+        outputs = [ "out" ];
+        buildCommand = ''
+          dir=$(dirname $relpath)
+          mkdir -p $dir out/$dir
+          if [ -d $src ]; then cp -r $src/. $dir/; else cp $src $leanPath; fi
+          alectryon --frontend lean4+markup $leanPath --backend webpage -o $out/$leanPath.md
+        '';
+      });
+
+      renderPackage = pkg: symlinkJoin {
+        name = "${pkg.name}-mds";
+        paths = map renderLeanMod (lib.attrValues pkg.mods);
+      };
+
+      literate = buildLeanPackage {
+        name = "literate";
+        src = ./.;
+        roots = [ ];
+      };
+      inked = renderPackage literate;
+      doc = book;
+    };
+    defaultPackage = self.packages.${system}.doc;
+  });
+}
diff --git a/docs/user/src/README.md b/docs/user/src/README.md
new file mode 100644
index 000000000..fa1cac5c6
--- /dev/null
+++ b/docs/user/src/README.md
@@ -0,0 +1,16 @@
+# Introduction to Aeneas
+
+Aeneas is a verification toolchain for Rust programs aiming to embed purely functional translation of Rust programs into theorem provers such as Coq or Lean.
+
+## What it can do?
+
+Aeneas aims to provide verification facilities for **safe** Rust with some caveats described in the next section.
+
+## What it cannot do?
+
+- loops: no nested loops for now. We are working on lifting this limitation.
+- no functions pointers/closures: ongoing work. We have support for traits and will have support for function pointers and closures soon.
+- limited type parametricity: it is not possible for now to instantiate a type parameter with a type containing a borrow. This is mostly an engineering issue.
+- no nested borrows in function signatures: ongoing work.
+- interior mutability: ongoing work. We are thinking of modeling the effects of interior mutability by using ghost states.
+- no concurrent execution: long-term effort. We plan to address coarse-grained parallelism as a long-term goal.
diff --git a/docs/user/src/SUMMARY.md b/docs/user/src/SUMMARY.md
new file mode 100644
index 000000000..54a6905b9
--- /dev/null
+++ b/docs/user/src/SUMMARY.md
@@ -0,0 +1,11 @@
+# Summary
+
+[Introduction](./README.md)
+
+# Setup guide
+
+# Proving with Lean
+
+## Tactics guide
+
+- [Progress](./lean/tactics/progress.md)
diff --git a/docs/user/src/lean/tactics/progress.md b/docs/user/src/lean/tactics/progress.md
new file mode 100644
index 000000000..4617ec6cd
--- /dev/null
+++ b/docs/user/src/lean/tactics/progress.md
@@ -0,0 +1,2 @@
+# Progress
+
diff --git a/flake.nix b/flake.nix
index 37e977d4f..9b7717fb7 100644
--- a/flake.nix
+++ b/flake.nix
@@ -229,6 +229,7 @@
             pkgs.ocamlPackages.menhir
             pkgs.ocamlPackages.odoc
             pkgs.jq
+            pkgs.rustup
           ];
 
           inputsFrom = [