diff --git a/Cargo.lock b/Cargo.lock
index c902c6992..0b6542b48 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -893,11 +893,10 @@ dependencies = [
 
 [[package]]
 name = "num-bigint"
-version = "0.4.4"
+version = "0.4.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "608e7659b5c3d7cba262d894801b9ec9d00de989e8a82bd4bef91d08da45cdc0"
+checksum = "c165a9ab64cf766f73521c0dd2cfdff64f488b8f0b3e621face3462d3db536d7"
 dependencies = [
- "autocfg",
  "num-integer",
  "num-traits",
 ]
@@ -913,9 +912,9 @@ dependencies = [
 
 [[package]]
 name = "num-traits"
-version = "0.2.18"
+version = "0.2.19"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "da0df0e5185db44f69b44f26786fe401b6c293d1907744beaa7fa62b2e5a517a"
+checksum = "071dfc062690e90b734c0b2273ce72ad0ffa95f0c74596bc250dcfd960262841"
 dependencies = [
  "autocfg",
 ]
diff --git a/PUBLISHING.md b/PUBLISHING.md
index 78b2657a5..fd7e8bd59 100644
--- a/PUBLISHING.md
+++ b/PUBLISHING.md
@@ -8,6 +8,9 @@ Here is the list of the crates in this repository (excluding `tests`
 and `examples`):
 
 - `hax-test-harness` **(doesn't need to be published)**
+
+## cargo-hax
+
 1. `hax-frontend-exporter-options` (`frontend/exporter/options `)
 2. `hax-adt-into` (`frontend/exporter/adt-into`)
 3. `hax-frontend-exporter` (`frontend/exporter`)
@@ -15,13 +18,19 @@ and `examples`):
 5. `hax-diagnostics` (`frontend/diagnostics`)
 6. `hax-cli-options-engine` (`cli/options/engine`)
 7. `hax-subcommands` (binaries) (`cli/subcommands`)
-    - `cargo-hax`
-    - `hax-export-json-schemas`
-    - `hax-pretty-print-diagnostics`
-- `hax-lib-macros`
-- `hax-lint`
+   - `cargo-hax`
+   - `hax-export-json-schemas`
+   - `hax-pretty-print-diagnostics`
+
 - `hax-phase-debug-webapp`
 - `hax-driver`
 
+## hax-lib
+
+1. `hax-lib-macros-types`
+2. `hax-lib-macros`
+3. `hax-lib`
 
+---
 
+- `hax-lint`
diff --git a/hax-lib-macros/Cargo.toml b/hax-lib-macros/Cargo.toml
index 06605bd67..a2f4a5af4 100644
--- a/hax-lib-macros/Cargo.toml
+++ b/hax-lib-macros/Cargo.toml
@@ -6,7 +6,8 @@ license.workspace = true
 homepage.workspace = true
 edition.workspace = true
 repository.workspace = true
-readme.workspace = true
+readme = "README.md"
+description = "Hax-specific proc-macros for Rust programs"
 
 [lib]
 proc-macro = true
@@ -15,8 +16,13 @@ proc-macro = true
 proc-macro-error = "1.0.4"
 proc-macro2.workspace = true
 quote.workspace = true
+syn = { version = "2.0", features = [
+    "full",
+    "visit-mut",
+    "extra-traits",
+    "parsing",
+] }
 hax-lib-macros-types.workspace = true
-syn = { version = "2.0", features = ["full", "visit-mut", "extra-traits", "parsing"] }
 
 [dev-dependencies]
 hax-lib = { path = "../hax-lib" }
diff --git a/hax-lib-macros/README.md b/hax-lib-macros/README.md
new file mode 100644
index 000000000..d44b92856
--- /dev/null
+++ b/hax-lib-macros/README.md
@@ -0,0 +1,8 @@
+# hax proc macros
+
+Hax-specific proc-macros for Rust programs.
+
+This crate defines proc macros to be used in Rust programs that are extracted with
+hax.
+It provides proc macros such as `requires` and `ensures` to define pre- and post-conditions
+for functions.
diff --git a/hax-lib-macros/types/Cargo.toml b/hax-lib-macros/types/Cargo.toml
index ac2e56046..8f08a14c1 100644
--- a/hax-lib-macros/types/Cargo.toml
+++ b/hax-lib-macros/types/Cargo.toml
@@ -6,7 +6,8 @@ license.workspace = true
 homepage.workspace = true
 edition.workspace = true
 repository.workspace = true
-readme.workspace = true
+readme = "README.md"
+description = "Hax-internal types"
 
 [dependencies]
 serde.workspace = true
@@ -16,5 +17,3 @@ quote.workspace = true
 proc-macro2.workspace = true
 uuid = { version = "1.5", features = ["v4"] }
 
-[features]
-schemars = ["dep:schemars"]
diff --git a/hax-lib-macros/types/README.md b/hax-lib-macros/types/README.md
new file mode 100644
index 000000000..400538ddd
--- /dev/null
+++ b/hax-lib-macros/types/README.md
@@ -0,0 +1,3 @@
+# hax internal types
+
+A create with hax internal types.
diff --git a/hax-lib/Cargo.toml b/hax-lib/Cargo.toml
index 55b498617..299fd8b8e 100644
--- a/hax-lib/Cargo.toml
+++ b/hax-lib/Cargo.toml
@@ -9,8 +9,6 @@ repository.workspace = true
 readme = "README.md"
 description = "Hax-specific helpers for Rust programs"
 
-# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
-
 [dependencies]
 hax-lib-macros = { workspace = true, optional = true }
 num-bigint = { version = "0.4.3", default-features = false }
diff --git a/hax-lib/README.md b/hax-lib/README.md
new file mode 100644
index 000000000..f2c850f09
--- /dev/null
+++ b/hax-lib/README.md
@@ -0,0 +1,17 @@
+# hax library
+
+This crate contains helpers that can be used when writing Rust code that is proven
+through the hax toolchain.
+
+**⚠️ The code in this crate has no effect when compiled without the `--cfg hax`.**
+
+## Examples:
+
+```rust
+fn sum(x: Vec<u32>, y: Vec<u32>) -> Vec<u32> {
+  hax_lib::assume!(x.len() == y.len());
+  hax_lib::assert!(hax_lib::forall(|i: usize| hax_lib::implies(i < x.len(), || x[i] < 4242)));
+  hax_lib::debug_assert!(hax_lib::exists(|i: usize| hax_lib::implies(i < x.len(), || x[i] > 123)));
+  x.into_iter().zip(y.into_iter()).map(|(x, y)| x + y).collect()
+}
+```