diff --git a/Cargo.toml b/Cargo.toml
index 9914ef499..ea7eb8493 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -79,3 +79,6 @@ hax-lib-macros-types = { path = "hax-lib/macros/types", version = "=0.1.0-rc.1"
 hax-lib = { path = "hax-lib", version = "=0.1.0-rc.1" }
 hax-engine-names = { path = "engine/names", version = "=0.1.0-rc.1" }
 hax-types = { path = "hax-types", version = "=0.1.0-rc.1" }
+
+[workspace.metadata.release]
+owners = ["github:hacspec:crates"]
\ No newline at end of file
diff --git a/PUBLISHING.md b/PUBLISHING.md
index ae1491466..e671dbe78 100644
--- a/PUBLISHING.md
+++ b/PUBLISHING.md
@@ -1,4 +1,14 @@
-# Crates publishing
+# Publishing
+
+## OCaml
+
+There is only the package `hax-engine`, that includes a binary and a
+number of libraries.
+
+We have no particular release procedure for the engine: we don't plan
+on publishing it to opam.
+
+## Rust
 
 This repository is divided into several crates, some to be published,
 some not. All crates should start with the `hax-` prefix, but
@@ -9,7 +19,7 @@ and `examples`):
 
 - `hax-test-harness` **(doesn't need to be published)**
 
-## cargo-hax
+### cargo-hax
 
 1. `hax-frontend-exporter-options` (`frontend/exporter/options `)
 2. `hax-adt-into` (`frontend/exporter/adt-into`)
@@ -20,23 +30,31 @@ and `examples`):
    - `hax-export-json-schemas`
    - `hax-pretty-print-diagnostics`
 
-- `hax-phase-debug-webapp`
 - `hax-driver`
 
+### hax-lib
 
-## hax-lib
+We publish the following crates that are helper libraries to be used
+for hax code:
 
 1. `hax-lib-macros-types`
 2. `hax-lib-macros`
 3. `hax-lib`
 
----
-
-- `hax-lint`
-
-## Supporting crates for the engine
+### Supporting crates for the engine
 The crate listed below are used only by the OCaml build of the
 engine. Those should not be published on `crate.io`.
 
 1. `cargo-hax-engine-names`
 2. `cargo-hax-engine-names-extract`
+
+## Procedure
+ 1. Bump the version number with `cargo release LEVEL --no-publish --execute` (`cargo release --help` for more details on `LEVEL`). This will bump the version of every Rust crate, but also the version in `engine/dune-project`. This will also regenerate `engine/hax-engine.opam`. Note this will *not* publish the crate.
+ 2. PR the change
+ 3. when the PR is merged in main, checkout `main` and run `cargo release --execute`
+
+Note: for now, we are not publishing to Opam. Instead, let's just advertise the following for installation:
+```bash
+opam pin hax-engine https://github.com/hacspec/hax.git#the-release-tag
+opam install hax-engine
+```
diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md
index e5f094882..1201418f5 100644
--- a/book/src/SUMMARY.md
+++ b/book/src/SUMMARY.md
@@ -19,7 +19,7 @@
     - [Command line usage]()
        - [The include flag: which items should be extracted, and how?](faq/include-flags.md)
 - [Contributing]()
-    - [Structure]()
+    - [Architecture](contributing/architecture.md)
     - [Hax Cargo subcommand]()
     - [Frontend: the Rustc driver]()
     - [Frontend: the exporter]()
diff --git a/book/src/contributing/architecture.md b/book/src/contributing/architecture.md
new file mode 100644
index 000000000..4877c97fd
--- /dev/null
+++ b/book/src/contributing/architecture.md
@@ -0,0 +1,83 @@
+# Architecture
+
+Hax is a software pipeline designed to transform Rust code into various formal verification backends such as **F\***, **Coq**, **ProVerif**, and **EasyCrypt**. It comprises two main components:
+
+1. **The Frontend** (written in Rust)
+2. **The Engine** (written in OCaml)
+
+The frontend hooks into the Rust compiler, producing a abstract syntax tree for a given crate. The engine then takes this AST in input, applies various transformation, to reach in the end the language of the backend: F*, Coq...
+
+## The Frontend (Rust)
+
+The frontend is responsible for extracting and exporting Rust code's abstract syntax trees (ASTs) in a format suitable for processing by the engine (or by other tools).
+
+### [`hax-frontend-exporter` Library](https://hacspec.org/hax/frontend/hax_frontend_exporter/index.html)
+
+This library mirrors the internal types of the Rust compiler (`rustc`) that constitute the **HIR** (High-Level Intermediate Representation), **THIR** (Typed High-Level Intermediate Representation), and **MIR** (Mid-Level Intermediate Representation) ASTs. It extends them with additional information such as attributes, trait implementations, and removes ID indirections.
+
+**`SInto` Trait:** The library defines an entry point for translating a given `rustc` value to its mirrored hax version using the [`SInto`](https://hacspec.org/hax/frontend/hax_frontend_exporter/trait.SInto.html) trait (stateful `into`). For a value `x` of type `T` from `rustc`, if `T` is mirrored by hax, then `x.sinto(s)` produces an augmented and simplified "hax-ified" AST for `x`. Here, `s` represents the state holding information about the translation process.
+
+### `hax-driver` Binary
+
+`hax-driver` is a custom Rust compiler driver that behaves like `rustc` but performs additional tasks:
+
+1. **Item Enumeration:** Lists all items in a crate.
+2. **AST Transformation:** Applies `sinto` on each item to generate the hax-ified AST.
+3. **Output Generation:** Outputs the mirrored items into a `haxmeta` file within the `target` directory.
+
+### `cargo-hax` Binary
+
+`cargo-hax` provides a `hax` subcommand for Cargo, accessible via `cargo hax --help`. It serves as the command-line interface for hax, orchestrating both the frontend and the engine.
+
+**Workflow:**
+
+1. **Custom Build Execution:** Runs `cargo build`, instructing Cargo to use `hax-driver` instead of `rustc`.
+2. **Multiple Compiler Invocations:** `cargo build` invokes `hax-driver` multiple times with various options.
+3. **Inter-Process Communication:** `hax-driver` communicates with `cargo-hax` via `stderr` using JSON lines.
+4. **Metadata Generation:** Produces `haxmeta` files containing the transformed ASTs.
+5. **Engine Invocation (Optional):** If requested, runs the engine, passing options and `haxmeta` information via `stdin` serialized as JSON.
+6. **Interactive Communication:** Engages in interactive communication with the engine.
+7. **User Reporting:** Outputs results and diagnostics to the user.
+
+## The Engine (OCaml - [documentation](https://hacspec.org/hax/engine/hax-engine/index.html))
+
+The engine processes the transformed ASTs and options provided via JSON input from `stdin`. It performs several key functions to convert the hax-ified Rust code into the target backend language.
+
+### Importing and Simplifying ASTs
+
+- **AST Importation:** Imports the hax-ified Rust THIR AST. This is module [`Import_thir`](https://hacspec.org/hax/engine/hax-engine/Hax_engine/Import_thir/index.html).
+- **Internal AST Conversion:** Converts the imported AST into a simplified and opinionated internal AST designed for ease of transformation and analysis. This is mostly the functor [`Ast.Make`](https://hacspec.org/hax/engine/hax-engine/Hax_engine/Ast/Make/index.html).
+
+### Internal AST and Features
+
+The internal AST is defined using a **functor** that takes a list of type-level booleans, referred to as **features**, and produces the AST types accordingly.
+
+Features are for instances, mutation, loops, unsafe code. The enumeration [`Features.Enumeration`](https://hacspec.org/hax/engine/hax-engine/Hax_engine/Features/Enumeration/index.html) lists all those features.
+
+**Feature Witnesses:** On relevant AST nodes, feature witnesses are included to enforce constraints at the type level. For example, in the `loop` expression constructor, a witness of type `F.loop` is used, where `F` represents the current feature set. If `F.loop` is an empty type, constructing a `loop` expression is prohibited, ensuring that loops are disallowed in contexts where they are not supported.
+
+### Transformation Phases
+
+The engine executes a sequence of **phases**, which are determined based on the target backend. Each phase:
+
+1. **Input:** Takes a list of items from an AST with specific feature constraints.
+2. **Output:** Transforms these items into a new AST type, potentially enabling or disabling features through type-level changes.
+
+The phases can be found in the [`Phases`](https://hacspec.org/hax/engine/hax-engine/Hax_engine/Phases/index.html) module.
+
+### Backend Code Generation
+
+After completing the transformation phases:
+
+1. **Backend Printer Invocation:** Calls the printer associated with the selected backend to generate the target code.
+2. **File Map Creation:** Produces a map from file names to their contents, representing the generated code.
+3. **Output Serialization:** Outputs the file map and additional information (e.g., errors) as JSON to `stderr`.
+
+### Communication Protocol
+
+The engine communicates asynchronously with the frontend using a protocol defined in [`hax_types::engine_api::protocol`](https://hacspec.org/hax/frontend/hax_types/engine_api/protocol/index.html). This communication includes:
+
+- **Diagnostic Data:** Sending error messages, warnings, and other diagnostics.
+- **Profiling Information:** Providing performance metrics and profiling data.
+- **Pretty-Printing Requests:** Requesting formatted versions of Rust source code or diagnostics for better readability.
+
diff --git a/book/src/contributing/structure.md b/book/src/contributing/structure.md
deleted file mode 100644
index e69de29bb..000000000
diff --git a/cli/subcommands/Cargo.toml b/cli/subcommands/Cargo.toml
index 91512f584..9ba434912 100644
--- a/cli/subcommands/Cargo.toml
+++ b/cli/subcommands/Cargo.toml
@@ -54,6 +54,9 @@ hax-lib-macros-types = {workspace = true, features = ["schemars"]}
 version_check = "0.9"
 toml = "0.8"
 
+[package.metadata.release]
+pre-release-hook = ["dune", "build", "--root", "../../engine", "hax-engine.opam"]
+
 [[package.metadata.release.pre-release-replacements]]
 file = "../../engine/dune-project"
 search = "version [a-z0-9\\.-]+"
diff --git a/engine/names/Cargo.toml b/engine/names/Cargo.toml
index efc92fca6..58ebcb0d2 100644
--- a/engine/names/Cargo.toml
+++ b/engine/names/Cargo.toml
@@ -12,3 +12,6 @@ description = "Dummy crate containing all the Rust names the hax engine should b
 [dependencies]
 hax-lib-protocol = {path = "../../hax-lib-protocol"}
 hax-lib = {path = "../../hax-lib"}
+
+[package.metadata.release]
+release = false
diff --git a/engine/names/extract/Cargo.toml b/engine/names/extract/Cargo.toml
index 22604c874..ed24a9d3d 100644
--- a/engine/names/extract/Cargo.toml
+++ b/engine/names/extract/Cargo.toml
@@ -23,3 +23,6 @@ extract_names_mode = []
 
 [lints.rust]
 unexpected_cfgs = { level = "warn", check-cfg = ['cfg(feature, values("rustc"))'] }
+
+[package.metadata.release]
+release = false
diff --git a/hax-lib-protocol-macros/Cargo.toml b/hax-lib-protocol-macros/Cargo.toml
index de9561465..739fd467f 100644
--- a/hax-lib-protocol-macros/Cargo.toml
+++ b/hax-lib-protocol-macros/Cargo.toml
@@ -21,3 +21,6 @@ syn = { version = "2.0", features = [
     "extra-traits",
     "parsing",
 ] }
+
+[package.metadata.release]
+release = false
diff --git a/hax-lib-protocol/Cargo.toml b/hax-lib-protocol/Cargo.toml
index 0dee6ef9e..e442033b1 100644
--- a/hax-lib-protocol/Cargo.toml
+++ b/hax-lib-protocol/Cargo.toml
@@ -10,3 +10,6 @@ readme.workspace = true
 
 [dependencies]
 libcrux = "0.0.2-pre.2"
+
+[package.metadata.release]
+release = false
diff --git a/test-harness/Cargo.toml b/test-harness/Cargo.toml
index e0dbfe4ca..a11bb3e9d 100644
--- a/test-harness/Cargo.toml
+++ b/test-harness/Cargo.toml
@@ -25,3 +25,6 @@ insta = {version = "1.29.0", features = ["filters", "toml"]}
 serde = { version = "1.0", features = ["derive"] }
 regex = "1"
 hax-types.workspace = true
+
+[package.metadata.release]
+release = false