diff --git a/.markdownlint.json b/.markdownlint.json
new file mode 100644
index 0000000..8e1eca2
--- /dev/null
+++ b/.markdownlint.json
@@ -0,0 +1,3 @@
+{
+  "MD013": { "line_length": 120, "tables": false }
+}
diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml
index 74aadb4..ecede80 100644
--- a/.pre-commit-config.yaml
+++ b/.pre-commit-config.yaml
@@ -37,6 +37,11 @@ repos:
     hooks:
       - id: cargo-machete
         args: ["rust/"]
+  - repo: https://github.com/igorshubovych/markdownlint-cli
+    rev: e72a3ca1632f0b11a07d171449fe447a7ff6795e # v0.48.0
+    hooks:
+      - id: markdownlint
+        args: ["-f"]
   - repo: local
     hooks:
       - id: cargo-hack-check
diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
index 0000000..6bc6efd
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,70 @@
+# Changelog
+
+All notable changes to this project will be documented in this file.
+
+## [0.5.0] — 2026-05-25
+
+### Added
+
+- **Circuits as static libraries** (#16)
+
+   The central change in this release. Previously, witness generation required spawning a compiled executable per circuit.
+
+   Each circuit is now a linkable static archive (`lib{circuit}.a`) with a stable C FFI.
+
+   Two entry points per circuit:
+  - `{circuit}_generate_witness(WitnessInput*, Bytes*)`: Generates a witness in memory from a
+     JSON input string and an embedded `.dat` buffer; the caller owns the output buffer.
+  - `{circuit}_generate_witness_from_files(dat, inputs, output)`: Generates a witness from a `.dat` file and a JSON
+     input file, writing the witness to an output file.
+
+   The Rust crates (`lbc-{circuit}-sys`) wrap this FFI directly and can either link against a local build or download a
+   prebuilt release automatically.
+
+   See [`rust/README.md`](rust/README.md) for usage.
+
+- **Bundled static GMP** (#19)
+
+   `libgmp` is now compiled from source and statically linked, removing the runtime dependency on a system GMP
+   installation, and standardizing the GMP version used across all platforms.
+
+- **Older glibc compatibility** (#21)
+
+   Linux builds now target an older glibc ABI for broader distribution support.
+
+- **Dual MIT/Apache-2.0 license**.
+
+### Fixed
+
+- **Symbol resolution conflicts** (#22, #28, #29)
+
+   When multiple circuit libraries are linked into the same binary, the linker silently collapsed shared internal
+   symbols to a single definition, corrupting witness parsing and causing SIGSEGV.
+
+   See [CONTRIBUTING.md](CONTRIBUTING.md#symbol-isolation-in-circuit-libraries) for a full explanation and maintenance
+   notes.
+
+- **macOS C++ library linkage** (#27)
+
+   Fixed missing C++ standard library on macOS builds.
+
+- **Circuit assert statements** (#26)
+
+   Assert statements in the circuit source assumed standalone binary execution, causing disruptions when compiled as a library.
+
+- **Comparator full less-than**
+
+   Fixed incorrect output in the full less-than comparator circuit.
+
+### Housekeeping
+
+- Auto-update Nix hashes on release (#25)
+- Incremental builds (#20)
+- Pinned CI action versions (#24)
+- `rustfmt` configuration (#23)
+- GMP version consistency (#31)
+- String formatting fix (#30)
+
+---
+
+*No changelog was kept prior to v0.5.0.*
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 11706ec..ff4349b 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -4,21 +4,34 @@
 
 ### Prerequisites
 
-- [Rust](https://rustup.rs/) — the pinned toolchain version is in `rust-toolchain.toml` and will be installed automatically by `rustup`.
-- [pre-commit](https://pre-commit.com/) — used to run formatting, linting, and audit checks before each commit.
-- `llvm-objcopy` — required to build circuit static libraries (symbol isolation). On macOS, install via `brew install llvm` (LLVM 20+ required).
+#### Sys development
 
-### Installing the Pre-Commit Hooks
+- [Rust](https://rustup.rs/) — the pinned toolchain version is in `rust-toolchain.toml` and will be installed
+   automatically by `rustup`.
+- Compiled circuit libraries (`.a` files and `witness_generator.dat`) — see [rust/README.md](rust/README.md) for how to
+   provide them.
+
+#### Building circuits
+
+- `llvm-objcopy` — required for symbol isolation when building circuit static libraries. On macOS, install via `brew
+   install llvm` (LLVM 20+ required).
+
+### Pre-Commit
+
+[pre-commit](https://pre-commit.com/) covers most of the lints required by CI. It's not mandatory — you can run checks
+however you like — but it's the easiest way to catch issues before pushing.
+
+#### Installation
 
 ```bash
 pre-commit install
 ```
 
-This only needs to be done once after cloning the repo. Hooks will then run automatically on `git commit`.
+After this, they will be run automatically on every commit.
 
-### Running Checks Manually
+#### Running Manually
 
-To run all hooks manually against all files:
+To run the checks manually against all files:
 
 ```bash
 pre-commit run --all-files
@@ -28,169 +41,135 @@ pre-commit run --all-files
 
 #### Rust Toolchain
 
-When bumping the stable toolchain, update `channel` in `rust-toolchain.toml`. The comment there lists every other place that must be updated in sync (nightly version, CI workflows, pre-commit hooks).
+When bumping the stable toolchain, update `channel` in `rust-toolchain.toml`.
+The comment there lists every other place that must be updated in sync (nightly version, CI workflows, pre-commit hooks).
 
 #### Tool Versions
 
 `taplo`, `cargo-deny`, and `cargo-machete` are pinned in two places that must stay in sync:
+
 - `.pre-commit-config.yaml` (hook `rev`)
 - `.github/workflows/lint.yml` (`cargo install --version`)
 
 ---
 
-## Symbol Isolation in Circuit Libraries
+## Building
 
-Each circuit (PoQ, PoL, PoC, Signature) is compiled into a static archive (`libpoq.a`, `libpol.a`, etc.). 
-All four archives share the same internal C++ runtime — `loadCircuit`, `get_size_of_witness`, the `fr_*` field 
-arithmetic functions, `calcwit_*` functions, and others. They are compiled from the same source files but with 
-**different constant values per circuit** (e.g. `get_size_of_witness()` returns 18149 for PoQ and 20531 for PoL).
+For a full walkthrough of the CI build steps, from `.circom` source to release artifacts, see
+[docs/build-pipeline.md](docs/build-pipeline.md).
 
-### The Problem
+### Symbol Isolation in Circuit Libraries
 
-When two or more circuit libraries are linked into the same binary, the linker silently picks the first definition 
-it encounters for each symbol and discards the rest. 
-No error, no warning. 
-The result is that one circuit's constants end up hardwired into functions shared by both circuits, corrupting witness 
-parsing. 
-In practice: the wrong `get_size_of_witness()` value causes `loadCircuit` to compute an incorrect buffer size, `pu32` 
+#### The Problem
+
+Each circuit (PoQ, PoL, PoC, Signature) is compiled into a static archive (`libpoq.a`, `libpol.a`, etc.).
+All archives share the same symbols, compiled from the same source files but with **different
+constant values per circuit** (e.g. `get_size_of_witness()` returns 18149 for PoQ and 20531 for PoL).
+When two or more circuit libraries are linked into the same binary, the linker silently picks the first definition it
+encounters for each symbol and discards the rest without any sort of error or warning.
+The result is that one circuit's constants end up hardwired into functions shared by both circuits, corrupting witness
+parsing.
+In practice: the wrong `get_size_of_witness()` value causes `loadCircuit` to compute an incorrect buffer size, `pu32`
 walks off the end of the buffer, reads garbage as a length field, and the subsequent `memcpy` reads past the stack guard
 page, which results in a **SIGSEGV**.
 
-### The Fix
+#### The Fix
 
-The Makefile's `$(LIB)` rule uses a two-step process to localize all circuit-specific code before archiving:
+The Makefile uses a two-step process to hide all circuit-specific symbols before archiving:
 
-1. **Partial link** (`ld -r`): merges all circuit-specific `.o` files — everything except `fr.o` (pure field
-arithmetic, no circuit-specific calls) — into a single relocatable object. No symbols are resolved yet; this is
-consolidation only.
-2. **Symbol localization** (`llvm-objcopy --keep-global-symbol` / `objcopy --keep-global-symbol`): demotes every global symbol to local *except* the
-circuit's two public FFI entry points (`$(PROJECT)_generate_witness` and `$(PROJECT)_generate_witness_from_files`).
-Local symbols are invisible to the final linker, so each archive retains a private copy of every internal symbol — no
-conflict is possible regardless of how many circuits are linked together.
+1. **Partial link** (`ld -r`): merges all circuit-specific `.o` files into a single relocatable
+   object. `fr.o` is excluded — it contains only field arithmetic with no circuit-specific calls
+   and is safe to deduplicate across circuits.
+2. **Symbol localization**: demotes every global symbol to local except the two public FFI entry
+   points (`$(PROJECT)_generate_witness` and `$(PROJECT)_generate_witness_from_files`). Local
+   symbols are invisible to the final linker, so each archive retains a private copy.
 
-`llvm-objcopy` is required rather than GNU `objcopy`. GNU `objcopy` only changes the binding of COMDAT signature
-symbols to local, which confuses the linker's deduplication logic and causes "relocation refers to symbol in discarded
-section" errors. `llvm-objcopy` additionally clears the `GRP_COMDAT` flag on affected section groups, turning them into
-regular non-COMDAT sections that are simply kept as-is rather than deduplicated. The result is a slightly larger binary
-(each circuit keeps its own copy of shared template instantiations), but no linker errors.
+**`llvm-objcopy` vs GNU `objcopy`**
 
-`fr.o` is excluded from the merge because it contains only field arithmetic (`Fr_*`) with no circuit-specific calls.
-It is safe to deduplicate across circuits — the linker picks one copy, which is correct since the code is identical.
+`llvm-objcopy` is required on Linux. GNU `objcopy` only changes the binding of COMDAT signature
+symbols to local, confusing the linker's deduplication logic and causing "relocation refers to
+symbol in discarded section" errors. `llvm-objcopy` additionally clears the `GRP_COMDAT` flag,
+turning affected sections into regular non-COMDAT sections. Slightly larger binary, no linker errors.
 
-On macOS/Mach-O, `llvm-objcopy` (from `brew install llvm`) is used — it supports `--keep-global-symbol` for
-Mach-O since LLVM 20. It is not available in Xcode's toolchain and must be installed separately.
-Mach-O prepends an underscore to every C symbol (`poc_generate_witness` → `_poc_generate_witness`),
-so `--keep-global-symbol` arguments must include the leading `_`. The Makefile's `SYM_PREFIX` variable
-handles this: it is set to `_` on macOS and empty on other platforms.
+##### macOS
 
-On Windows, GNU `objcopy` (from MinGW binutils) is used instead of `llvm-objcopy`. `llvm-objcopy --keep-global-symbol`
-is not supported for COFF objects, but GNU `objcopy --keep-global-symbol` works correctly on COFF — it maps the local
-binding to COFF storage class `C_STAT`. The ELF `GRP_COMDAT` problem that required `llvm-objcopy` on Linux does not
-apply on Windows: COFF COMDAT is per-section rather than group-based, and the linker already deduplicates it
-automatically.
+Uses `llvm-objcopy` (from `brew install llvm`, LLVM 20+).
 
-### Maintenance
+Mach-O prepends `_` to every C symbol, so `--keep-global-symbol` arguments must include the
+leading `_`. The Makefile's `SYM_PREFIX` variable handles this automatically.
+
+##### Windows
+
+Uses GNU's `objcopy` (from MinGW binutils).
+
+GNU's `objcopy` works correctly on COFF, mapping local binding to storage class `C_STAT`.
+The ELF `GRP_COMDAT` problem doesn't apply: COFF COMDAT is per-section rather than group-based.
+
+#### FFI Maintenance
 
 `PUBLIC_SYMS` is hardcoded to `$(PROJECT)_generate_witness` and `$(PROJECT)_generate_witness_from_files` in the
-Makefile. If the public FFI API ever changes — entry points renamed or new ones added — update that variable,
-otherwise the affected symbols will be localized and linking will fail.
+Makefile. If the public FFI API ever changes — entry points renamed or new ones added — update that variable, otherwise
+the affected symbols will be localized and linking will fail.
 
 ---
 
-## Triggering a New Release for Logos Blockchain Circuits
+## Releasing
+
+### Triggering a Release Build
 
 To trigger a release build:
 
-1. Create and push a tag in the format `vX.Y.Z`.
+1. Create and push a tag in the format `vX.Y.Z`:
+
+   ```bash
+   git tag v1.2.3 -m "Release v1.2.3"
+   git push --tags
+   ```
+
 2. This will automatically trigger the `.github/workflows/build_circuits.yml` workflow.
 3. Once the workflow finishes, the generated artifacts will be attached to a new release.
 
-> Currently, releases published this way are marked as **Draft** and **Pre-Release** to ensure that the changelog and 
-> pre-release steps are manually reviewed first.
+> Pull Requests will also generate artifacts, which may be found on the job's page, but won't generate a new release.
 
-### Generated Artifacts
+#### Generated artifacts
 
-Each release includes a single unified bundle per platform:
+For each supported platform (Linux x86_64, Linux aarch64, macOS aarch64, Windows x86_64), a release artifact is
+generated:
 
-#### Unified Release Bundles
-
-For each supported platform (Linux x86_64, macOS aarch64, Windows x86_64):
-
-- **`logos-blockchain-circuits-{version}-{os}-{arch}.tar.gz`**
-
-  A complete bundle containing all components needed to generate and verify proofs for all circuits.
+**`logos-blockchain-circuits-{version}-{os}-{arch}.tar.gz`** — a complete bundle containing all components needed to
+generate and verify proofs for all circuits.
 
 **Bundle Structure:**
 
-```
+```text
 logos-blockchain-circuits-{version}-{os}-{arch}/
-├── VERSION
+├── lib/
+│   └── libgmp.a
+├── {circuit}/              (poc/, pol/, poq/, signature/)
+│   ├── include/
+│   ├── lib{circuit}.a
+│   ├── proving_key.zkey
+│   ├── verification_key.json
+│   └── witness_generator.dat
 ├── prover[.exe]
 ├── verifier[.exe]
-├── pol/
-│   ├── libpol.a
-│   ├── witness_generator.dat
-│   ├── include/
-│   ├── proving_key.zkey
-│   └── verification_key.json
-├── poq/
-│   ├── libpoq.a
-│   ├── witness_generator.dat
-│   ├── include/
-│   ├── proving_key.zkey
-│   └── verification_key.json
-├── signature/
-│   ├── libsignature.a
-│   ├── witness_generator.dat
-│   ├── include/
-│   ├── proving_key.zkey
-│   └── verification_key.json
-└── poc/
-    ├── libpoc.a
-    ├── witness_generator.dat
-    ├── include/
-    ├── proving_key.zkey
-    └── verification_key.json
+└── VERSION
 ```
 
-> On Windows, static libraries use the `.lib` extension instead of `.a` (e.g. `pol.lib`).
+> On Windows, static libraries use the `.lib` extension instead of `.a` (e.g. `pol.lib`, `gmp.lib`).
 
-At the root level:
-- **prover**: Rapidsnark prover binary for generating zk-SNARK proofs
-- **verifier**: Rapidsnark verifier binary for verifying proofs
+The proving keys are generated using the Hermez Powers of Tau ceremony — see [docs/build-pipeline.md § Step 2](docs/build-pipeline.md#step-2--proving-key-generation).
 
-Each circuit directory contains:
-- **lib{circuit}.a / {circuit}.lib**: Static library for generating witnesses from inputs
-- **witness_generator.dat**: Required data file for the witness generator
-- **include/**: C headers for linking against the witness generator library
-- **proving_key.zkey**: Groth16 proving key for generating zk-SNARK proofs
-- **verification_key.json**: Verification key for verifying proofs
+### Publishing
 
-The proving keys are generated using the Hermez Powers of Tau ceremony (`powersOfTau28_hez_final_17.ptau`), which supports circuits with up to 2^17 constraints.
-
-### Example
-
-```bash
-git tag v1.2.3 -m "Release v1.2.3"
-git push --tags
-```
-
-## Publishing the Release
-
-After triggering the release, it will appear as a **Draft** and **Pre-Release**.  
-Before making it public, make sure to:
+Releases are marked as **Draft** and **Pre-Release** to ensure the changelog and pre-release steps are manually reviewed
+before going public. Before publishing:
 
 1. **Review the changelog**  
    Ensure that all relevant changes are clearly listed and properly formatted.
 
 2. **Confirm the pre-release checklist**  
    Verify that all required steps have been completed, then remove the checklist from the release notes.
-
-Once everything looks good:
-
 3. **Mark the release as published**  
    - Uncheck **“This is a pre-release.”**  
    - Publish the release (removing the Draft state).
-
-> ⚡ **Important:** Logos Blockchain builds will only pick up the new circuits once the release is published as **Latest** (i.e. not marked as draft or pre-release).
-
diff --git a/README.md b/README.md
index 6b7fbbe..96506e9 100644
--- a/README.md
+++ b/README.md
@@ -1 +1,54 @@
 # Logos Blockchain Circuits
+
+ZK-SNARK circuits for the [Logos Blockchain](https://github.com/logos-blockchain/logos-blockchain), built with
+[Circom](https://docs.circom.io/) and distributed as linkable static libraries.
+
+## Circuits
+
+| Circuit                       | What it proves                                                    |
+|-------------------------------|-------------------------------------------------------------------|
+| **PoQ** — Proof of Quota      | A node has quota to participate in a blend session                |
+| **PoL** — Proof of Leadership | A note holder would win the leadership lottery for a given slot   |
+| **PoC** — Proof of Claim      | A voucher is validly owned and its nullifier is correctly derived |
+| **Signature**                 | Knowledge of secret keys and their corresponding public keys      |
+
+## Architecture
+
+```mermaid
+flowchart TD
+    A["Source circuit\n({circuit}.circom)"]
+    B("Circom compilation")
+    C["{circuit}_cpp/"]
+    R["{circuit}.r1cs"]
+    PK("Proving key generation")
+    Z["proving_key.zkey\nverification_key.json"]
+    DAT["{circuit}.dat"]
+    D["src/\n(circom_adapter, types, ...)"]
+    D2["src/{circuit}/ffi.cpp"]
+    E("Makefile")
+    F["lib{circuit}.a\nlibgmp.a"]
+    G["lbc-{circuit}-sys"]
+
+    A --> B -->|Generates| C
+    B -->|Generates| R --> PK --> Z
+    B -->|Generates| DAT
+    D -.-> C
+    D2 -.-> C
+    C --> E -->|Produces| F
+    F -->|Linked by| G
+    DAT -->|Embedded into| G
+```
+
+Each circuit is compiled from Circom source to C++, combined with shared common files (`circom_adapter`, `types`, ...)
+and a circuit-specific FFI layer (`src/{circuit}/ffi.cpp`), and built into a static library.
+
+The Rust sys crates link directly against these libraries.
+
+## Docs
+
+| Document                                         | What's in it                                               |
+|--------------------------------------------------|------------------------------------------------------------|
+| [CHANGELOG.md](CHANGELOG.md)                     | What changed and why, by version                           |
+| [CONTRIBUTING.md](CONTRIBUTING.md)               | Dev setup, build details, and release process              |
+| [rust/README.md](rust/README.md)                 | How to use the Rust sys crates                             |
+| [docs/build-pipeline.md](docs/build-pipeline.md) | CI build steps, from `.circom` source to release artifacts |
diff --git a/docs/build-pipeline.md b/docs/build-pipeline.md
new file mode 100644
index 0000000..a64671b
--- /dev/null
+++ b/docs/build-pipeline.md
@@ -0,0 +1,141 @@
+# Build Pipeline
+
+This document walks through the CI build steps, from `.circom` source to the full set of release artifacts.
+
+---
+
+## Overview
+
+| Step                                                                        | What happens                                                        |
+|-----------------------------------------------------------------------------|---------------------------------------------------------------------|
+| [1 — Circom compilation](#step-1--circom-compilation)                       | `.circom` source compiled to C++                                    |
+| [2 — Proving key generation](#step-2--proving-key-generation)               | `.r1cs` + `.ptau` → `.zkey` and `verification_key.json`             |
+| [3 — Patching `main.cpp`](#step-3--the-maincpp-return-patch)                | Fix missing `return` to prevent UB infinite loop                    |
+| [4 — The FFI layer](#step-4--the-ffi-layer)                                 | Common files and circuit-specific FFI layered into `{circuit}_cpp/` |
+| [5 — Compilation and linking](#step-5--compilation-and-linking)             | Compile with symbol isolation                                       |
+| [6 — The `.dat` file](#step-6--the-dat-file)                                | Binary circuit data embedded in the Rust crate at compile time      |
+| [7 — GMP](#step-7--gmp)                                                     | Bundled static `libgmp.a` used instead of system GMP                |
+| [8 — Rust build script](#step-8--rust-build-script)                         | Resolves library paths, emits Cargo link directives                 |
+| [9 — Rapidsnark](#step-9--rapidsnark)                                       | Prover and verifier binaries built and bundled                      |
+
+---
+
+## Step 1 — Circom compilation
+
+Produces three outputs:
+
+- `{circuit}_cpp/` — C++ source files for the witness generator.
+- `{circuit}.r1cs` — the constraint system, used for proving key generation.
+- `{circuit}.dat` — binary circuit data.
+
+---
+
+## Step 2 — Proving key generation
+
+The `.r1cs` from Step 1 is combined with the Hermez Powers of Tau ceremony file to produce:
+
+- `proving_key.zkey` — Groth16 proving key, used by the prover to generate proofs.
+- `verification_key.json` — used to verify proofs.
+
+---
+
+## Step 3 — The `main.cpp` return patch
+
+Immediately after circom runs, the build patches `main.cpp` to insert a `return 0;` at the end of `main()`.
+
+**Why**: The FFI layer calls circom's `main()` directly, which is already technically UB in C++ (calling `main` directly
+is forbidden by the standard). On top of that, circom generates `main()` with no explicit `return` on the success path.
+
+With `-O3`, the compiler treats the missing `return` as undefined behaviour and can optimise the entire success path
+into an infinite loop.
+
+---
+
+## Step 4 — The FFI layer
+
+Circom's generated C++ has no stable external API, the FFI layer adds one.
+It consists of two groups of files copied into `{circuit}_cpp/` before compilation:
+
+- **Common adapter files** (`circom_adapter`, `types`, `circom_fwd`, `assert.h`): Bridge the
+  circom internals to a stable C ABI, shared across all circuits.
+- **Circuit-specific entry points** (`src/{circuit}/ffi.cpp`): The public `extern "C"` functions
+  that become the library's API.
+
+```text
+src/
+  types.hpp           → copied into {circuit}_cpp/
+  circom_adapter.cpp  → copied into {circuit}_cpp/
+  circom_adapter.hpp  → copied into {circuit}_cpp/
+  circom_fwd.hpp      → copied into {circuit}_cpp/
+  assert.h            → copied into {circuit}_cpp/
+  {circuit}/
+    ffi.cpp           → copied into {circuit}_cpp/{circuit}/
+    ffi.hpp           → copied into {circuit}_cpp/{circuit}/
+```
+
+---
+
+## Step 5 — Compilation and linking
+
+### Compilation
+
+All sources are compiled with `-Dmain=circom_main` (alongside standard flags), with bundled GMP
+headers prepended before the system include path — see [Step 7](#step-7--gmp).
+
+### Symbol isolation
+
+All circuits compile the same internal functions (`loadCircuit`, `get_size_of_witness`, etc.) from the same source, but
+with different circuit-specific constants. When multiple circuits are linked into the same binary, the linker silently
+picks one definition per symbol and discards the rest, mixing constants across circuits and corrupting witness
+generation.
+
+To prevent this, every internal symbol is hidden: circuit objects are merged into a single
+relocatable object, then all symbols except the two public entry points are demoted to local.
+Local symbols are invisible to the final linker, so each circuit keeps its own private copy.
+
+`fr.o` is the exception: it stays global and is added to the archive separately since it doesn't vary between circuits.
+
+See [CONTRIBUTING.md § Symbol Isolation](../CONTRIBUTING.md#symbol-isolation-in-circuit-libraries) for the full
+explanation and implementation details.
+
+---
+
+## Step 6 — The `.dat` file
+
+`{circuit}.dat` (produced in Step 1) is embedded in the Rust crate at compile time.
+
+---
+
+## Step 7 — GMP
+
+To standardise the GMP version used by all circuits, `libgmp.a` is built from source as part of
+the CI build and placed in a `lib/` directory alongside the circuit artifacts. CI sets
+include/link flags to point at the bundled GMP before any system path, ensuring it takes priority.
+
+---
+
+## Step 8 — Rust build script
+
+Each `-sys` crate delegates its `build.rs` to `lbc_build`, which resolves the library paths,
+links `lib{circuit}.a` and `libgmp.a` into Cargo, and re-exports the path to
+`witness_generator.dat` for compile-time embedding. See [rust/README.md](../rust/README.md).
+
+---
+
+## Step 9 — Rapidsnark
+
+The `prover` and `verifier` binaries are built from the rapidsnark submodule and bundled with
+the release artifacts alongside the circuit libraries.
+
+---
+
+## Regenerating a circuit
+
+If you change a `.circom` source file:
+
+1. Recompile the circuit and rebuild the library.
+2. Update the proving key if the R1CS changed — a changed `.circom` almost always changes the
+   R1CS, which invalidates the existing `.zkey`.
+
+If you add a new public FFI entry point to `src/{circuit}/ffi.hpp`, update `PUBLIC_SYMS` in the
+Makefile. Any symbol not listed there will be localised and the linker will fail to find it.
diff --git a/rust/README.md b/rust/README.md
index 2bdf187..c38448e 100644
--- a/rust/README.md
+++ b/rust/README.md
@@ -1,2 +1,99 @@
-# Logos Blockchain Circuits – Rust
-This directory contains the Rust FFI to interact with the Logos Blockchain Circuits.
+# Logos Blockchain Circuits — Rust
+
+Rust bindings for the Logos Blockchain Circuits.
+
+Each circuit has a `-sys` crate that wraps the underlying C FFI with a safe Rust API.
+
+## Crates
+
+| Crate               | Description                                     |
+|---------------------|-------------------------------------------------|
+| `lbc-poq-sys`       | Witness generator for PoQ (Proof of Quota)      |
+| `lbc-pol-sys`       | Witness generator for PoL (Proof of Leadership) |
+| `lbc-poc-sys`       | Witness generator for PoC (Proof of Claim)      |
+| `lbc-signature-sys` | Witness generator for Signature                 |
+| `lbc-types`         | Shared types                                    |
+| `lbc-build`         | Build helper                                    |
+
+## Providing the circuit libraries
+
+Each `-sys` crate needs the compiled circuit library directory for its circuit, containing `lib{circuit}.a` and `witness_generator.dat`.
+There are two ways to provide it, detailed below.
+
+### Option A — Prebuilt download
+
+Enable the `prebuilt` Cargo feature.
+
+The build script downloads the release bundle matching the crate version from GitHub Releases and caches it locally.
+
+```toml
+[dependencies]
+lbc-poq-sys = { version = "0.5", features = ["prebuilt"] }
+```
+
+The cache location depends on the operating system:
+
+- Linux: `~/.cache/logos/blockchain/`
+- macOS: `~/Library/Caches/logos/blockchain/`
+- Windows: `%LOCALAPPDATA%\logos\blockchain\`
+
+The downloaded bundle version always matches `CARGO_PKG_VERSION`.
+
+### Option B — Custom path
+
+Point the build script at any directory containing the compiled circuit libraries:
+
+```bash
+LBC_POQ_LIB_DIR=/path/to/poq
+LBC_POL_LIB_DIR=/path/to/pol
+LBC_POC_LIB_DIR=/path/to/poc
+LBC_SIGNATURE_LIB_DIR=/path/to/signature
+LBC_LIB_DIR=/path/to/lib                 # Directory containing the required libs
+                                         # If using a release bundle, this is the included lib/ directory
+```
+
+> The `justfile` at the repo root contains recipes (`just poq`, `just pol`, etc.) that build the circuit libraries from
+> source.
+>
+> This is not yet an officially supported workflow, but it can serve as a reference if you need to produce the
+> libraries yourself.
+
+## Usage
+
+### In-memory witness generation
+
+```rust
+use lbc_poq_sys::native::{PoqWitnessInput, generate_witness};
+use lbc_types::native::{Error, Witness};
+
+fn main() -> Result<Witness, Error> {
+    let inputs_json = std::fs::read_to_string("poq-input.json").expect("failed to read input");
+    let input = PoqWitnessInput::new(inputs_json)?;
+    generate_witness(&input)
+}
+```
+
+### File-based witness generation
+
+```rust
+use lbc_poq_sys::native::generate_witness_from_files;
+use lbc_types::native::Error;
+use std::path::Path;
+
+fn main() -> Result<(), Error> {
+    generate_witness_from_files(
+        Path::new("/path/to/witness_generator"),  // Extensionless .dat file
+        Path::new("poq-input.json"),
+        Path::new("output.wtns"),
+    )?;
+    Ok(())
+}
+```
+
+The other circuits follow the same pattern under `lbc_pol_sys`, `lbc_poc_sys` and `lbc_signature_sys`.
+
+## Running tests
+
+```bash
+cargo test
+```