diff --git a/README.md b/README.md
index ae5a32a72..ec44db23e 100644
--- a/README.md
+++ b/README.md
@@ -2,34 +2,19 @@
-**The edge-native, zero-knowledge runtime and R1CS compilation toolkit.**
+[](https://github.com/worldfnd/provekit/actions)
+[](https://rustup.rs/)
+[](./License.md)
-[](https://github.com/atheon/provekit/actions)
-[](https://rustup.rs/)
-[](#)
-
-*Empowering developers to build lightweight, mobile-optimized cryptographic applications within the Noir and Gnark ecosystems.*
-
-[Explore the Docs](#-getting-started) · [Report Bug](../../issues) · [Request Feature](../../issues)
+[Getting Started](#getting-started) · [Examples](./noir-examples/) · [Contributing](./CONTRIBUTING.md) · [Issues](https://github.com/worldfnd/provekit/issues)
----
-
-## ✨ Why ProveKit?
-
-Developing cutting-edge cryptography for constrained edge devices demands more than generic tooling. **ProveKit** bridges the gap between high-level ZK languages and high-performance, mobile-first execution.
-
-- **📱 Edge-Optimized:** Zero compromises. ProveKit features bespoke memory management, custom allocators, and integrates natively with macOS `instruments`, `samply`, and `tracy` to guarantee an ultra-low footprint.
-- **⬛ Noir Native:** Built heavily on the [Noir](https://noir-lang.org/) stack. ProveKit consumes native Noir circuits, providing immediate interoperability.
-- **⚡ M31/CM31 First:** Leverages the `skyscraper` backend for ruthlessly efficient field arithmetic.
-- **🔄 Universal Recursion:** Gnark bindings allow you to take mobile-generated proofs and securely verify them on-chain via recursive rollups.
+ProveKit lets you take a Noir circuit, compile it to R1CS, and generate a WHIR proof. It's built for mobile and constrained environments and ships with a custom BN254 hash engine ([Skyscraper](skyscraper/)), swap-to-disk memory management, and C FFI for iOS and Android. If you need on-chain verification, there's a gnark recursive verifier that wraps proofs in Groth16.
---
-## 🏗️ Architecture
-
-ProveKit implements a highly decoupled pipeline—from constraint generation to proof verification.
+## Architecture
```mermaid
graph TD
@@ -60,45 +45,66 @@ graph TD
V -->|Validates| G
```
-### Module Landscape
+### Crates
-| Layer | Component | Description |
+| Layer | Crate | Description |
| :--- | :--- | :--- |
-| **Tooling** | `tooling/cli/` | The unified binary interface (`provekit-cli`). |
-| **Logic** | `provekit/prover/`
`provekit/verifier/` | Core ZK proving systems algorithms and verification targets. |
-| **Constraints** | `provekit/r1cs-compiler/` | Translates Noir execution environments down to R1CS formats. |
-| **Maths** | `skyscraper/` | Hand-optimized CM31/M31 field implementations. |
-| **Interops**| `tooling/provekit-gnark/`
`gnark-whir/`| Bridges gap between Rust proofs and Go / Gnark validations. |
+| CLI | `tooling/cli/` | `provekit-cli`: prepare, prove, verify, inspect |
+| Prover / Verifier | `provekit/prover/`
`provekit/verifier/` | WHIR sumcheck, witness solving, commitment |
+| Compiler | `provekit/r1cs-compiler/` | Noir ACIR → R1CS with constraint optimizations |
+| Hash engine | `skyscraper/` | Custom BN254 hash with SIMD-accelerated field arithmetic |
+| Interop | `tooling/provekit-gnark/`
`gnark-whir/` | Rust ↔ Go/gnark bridge for recursive verification |
---
-## 🚀 Getting Started
+## Example
+
+Here's [`noir-examples/basic`](./noir-examples/basic/), which proves knowledge of a Poseidon hash preimage:
-ProveKit tightly integrates with the Noir (`nargo`) development chain. Standard installation requires a strict cross-compatible version of the environment.
+```rust
+use dep::poseidon2;
+
+fn main(plains: [Field; 2], result: Field) {
+ let hash = poseidon2::bn254::hash_2(plains);
+ assert(hash == result);
+}
+```
+
+```sh
+cd noir-examples/basic
+nargo compile
+cargo run --release --bin provekit-cli prepare ./target/basic.json --pkp prover.pkp --pkv verifier.pkv
+cargo run --release --bin provekit-cli prove prover.pkp Prover.toml -o proof.np
+cargo run --release --bin provekit-cli verify verifier.pkv proof.np
+```
+
+---
+
+## Getting Started
+
+You need nargo `v1.0.0-beta.19` and Rust nightly. Toolchain is pinned in `rust-toolchain.toml`; rustup picks it up automatically.
-1️⃣ Setup Dependencies
+1. Install nargo
-Install the exact Noir version required by our bridging components:
```sh
noirup --version v1.0.0-beta.19
```
-*Tip: Ensure your Rust toolchain is on at least `1.75`.*
-2️⃣ Compile a Circuit
+2. Compile a circuit
-Our examples use `poseidon-rounds` as the canonical benchmark. You can use standard Noir or `mavros`.
+The steps below use `poseidon-rounds` as the example circuit.
-**A. Using nargo:**
+**With nargo:**
```sh
cd noir-examples/poseidon-rounds
nargo compile
cargo run --release --bin provekit-cli prepare ./target/basic.json --pkp ./prover.pkp --pkv ./verifier.pkv
```
-**B. Using mavros:**
+**With mavros** ([install instructions](https://github.com/reilabs/mavros)):
```sh
cd noir-examples/poseidon-rounds
mavros compile
@@ -107,75 +113,69 @@ cargo run --release --bin provekit-cli prepare --compiler mavros ./target/basic.
-3️⃣ Prove & Verify Workflow
-
-Once the constraint keys are extracted, run the high-performance prover:
+3. Prove and verify
```sh
-# Generate the dense ZK proof
cargo run --release --bin provekit-cli prove ./prover.pkp ./Prover.toml -o ./proof.np
-
-# Locally verify
cargo run --release --bin provekit-cli verify ./verifier.pkv ./proof.np
```
-**Generate inputs for the Gnark circuit & Recursively Verify:**
+**Recursive on-chain verification:**
```sh
cargo run --release --bin provekit-cli generate-gnark-inputs ./verifier.pkv ./proof.np
cd ../../recursive-verifier
-go run cmd/cli/main.go --config ../noir-examples/poseidon-rounds/params_for_recursive_verifier --r1cs ../noir-examples/poseidon-rounds/r1cs.json
+go run cmd/cli/main.go \
+ --config ../noir-examples/poseidon-rounds/params_for_recursive_verifier \
+ --r1cs ../noir-examples/poseidon-rounds/r1cs.json
```
-4️⃣ Benchmark Tooling
+4. Benchmark
-ProveKit can natively be benchmarked against alternative prover backends like [Barretenberg](https://github.com/AztecProtocol/aztec-packages/blob/master/barretenberg/bbup/README.md).
+Benchmark against [Barretenberg](https://github.com/AztecProtocol/aztec-packages/blob/master/barretenberg/bbup/README.md) with [hyperfine](https://github.com/sharkdp/hyperfine):
```sh
cd noir-examples/poseidon-rounds
cargo run --release --bin provekit-cli prepare ./target/basic.json --pkp ./prover.pkp --pkv ./verifier.pkv
-hyperfine 'nargo execute && bb prove -b ./target/basic.json -w ./target/basic.gz -o ./target' '../../target/release/provekit-cli prove ./prover.pkp ./Prover.toml'
+hyperfine \
+ 'nargo execute && bb prove -b ./target/basic.json -w ./target/basic.gz -o ./target' \
+ '../../target/release/provekit-cli prove ./prover.pkp ./Prover.toml'
```
-**Run internal benchmarks:**
+Internal benchmark suite:
```sh
cargo test -p provekit-bench --bench bench
```
-
---
-## 🛠️ Diagnostics & Profiling
-
-ProveKit exposes industry-grade telemetry specifically tuned for ensuring applications won't blow up a mobile app's RAM budget.
+## Profiling
-| Tooling Platform | Description & Command Structure |
-| :--- | :--- |
-| **Native Diagnostics** | Toggle internal allocators:
`cargo run --release --features profiling --bin provekit-cli prove ...` |
-| **Tracy GUI** | Requires instrumented binary build:
`cargo build --release --features profiling` *(Note: Use `dsymutil` on macOS)* |
-| **Samply (CPU)** | Native CPU Flamegraphs:
`samply record -r 10000 -- prove ...` |
-| **Apple Instruments** | Native macOS allocation tracking:
`cargo instruments --template Allocations --release --bin provekit-cli prove ...` |
+| Tool | Measures | Command |
+| :--- | :--- | :--- |
+| Built-in allocator stats | Memory | `cargo run --release --features profiling --bin provekit-cli prove ...` |
+| [Tracy](https://github.com/wolfpld/tracy) | CPU + memory (interactive GUI) | `cargo build --release --features profiling`, then run with Tracy listening. On macOS run `dsymutil` on the binary first for call stacks. |
+| [Samply](https://github.com/mstange/samply) | CPU flamegraphs | `samply record -r 10000 -- ./target/release/provekit-cli prove ...` |
+| [Instruments](https://crates.io/crates/cargo-instruments) | Allocations (macOS only) | `cargo instruments --template Allocations --release --bin provekit-cli prove ...` |
-> [!TIP]
-> **Static Analysis & Inspection:** You can bypass execution to statically measure proof density and investigate logic utilization using our CLI tools:
-> - `provekit-cli circuit_stats ./target/basic.json`
-> - `provekit-cli analyze-pkp ./prover.pkp`
-> - `provekit-cli show-inputs ./verifier.pkv ./proof.np`
+If you want to inspect without running a proof:
+```sh
+provekit-cli circuit_stats ./target/basic.json # constraint count and R1CS structure
+provekit-cli analyze-pkp ./prover.pkp # proving key size breakdown
+provekit-cli show-inputs ./verifier.pkv ./proof.np # public input names and values
+```
---
-## 📚 Related Projects
+## Acknowledgements
-Designed in lockstep with industry leaders. Be sure to explore integrated systems:
+- [**WHIR**](https://github.com/WizardOfMenlo/whir): the polynomial commitment scheme and sumcheck protocol the proof system is built on. `WhirR1CSScheme` wraps it for R1CS satisfiability over BN254.
-* [**🌪️ WHIR**](https://github.com/WizardOfMenlo/whir) — The underlying cryptography implementations.
-* [**🧽 Spongefish**](https://github.com/arkworks-rs/spongefish) — Core primitives from the `arkworks-rs` team.
-* [**⬛ Noir**](https://github.com/noir-lang/noir) — The zero-knowledge domain specific language proving stack.
+- [**Spongefish**](https://github.com/arkworks-rs/spongefish): Fiat-Shamir library from arkworks. All transcript construction and challenge derivation goes through its `DuplexSponge` API.
----
-
-Driven by research, built for production.
-
+- [**gnark-skyscraper**](https://github.com/reilabs/gnark-skyscraper): Go implementation of the Skyscraper hash. The recursive verifier needs it to reproduce the same Merkle commitments as the Rust prover.
+
+- [**Noir**](https://github.com/noir-lang/noir): the ZK DSL we compile from. Write your circuit in Noir, run nargo to get ACIR, and ProveKit handles the rest.