add a new readme

Author: oxarbitrage

README.md

@@ -1,6 +1,46 @@
 # The Zcash P2P Protocol Specification
 
-A TLA+ model for the zcash p2p network that follows https://zips.z.cash/zip-0204 
+A TLA+ formal specification of the Zcash peer-to-peer network protocol, following [ZIP-0204](https://zips.z.cash/zip-0204).
 
-- [protocol](protocol.tla)
+## Structure
+
+- [`messages.tla`](messages.tla) — Message constructors for all protocol messages (`version`, `verack`, `ping`, `pong`, `inv`, `getheaders`, `headers`, `getdata`, `block`).
+- [`protocol.tla`](protocol.tla) — Protocol actions, connection state machine, and liveness property.
+- [`protocol.cfg`](protocol.cfg) — TLC model checker configuration.
+
+## What is modeled
+
+The spec covers the connection lifecycle between peers:
+
+1. **Handshake** — `version` / `verack` exchange.
+2. **Keepalive** — `ping` / `pong` with nonce echo, triggered when a connection is idle.
+3. **Block sync** — `inv` → `getheaders` → `headers` → `getdata` → `block`, looping until the lagging peer catches up.
+
+Each connection is modeled as an explicit state machine with states:
+`init` → `version_sent` → `established` → `inv_sent` → `getheaders_sent` → `headers_sent` → `getdata_sent` ⇄ `block_received` → `synced`
+
+The spec verifies the **liveness property** `AllSynced`: eventually all peers reach the same block height (`<> ∀ i, j ∈ InitialPeers : nodes[i].blocks = nodes[j].blocks`).
+
+## Running the model checker
+
+Requires Java and [`tla2tools.jar`](https://github.com/tlaplus/tlaplus/releases/latest).
+
+```bash
+java -jar tla2tools.jar -config protocol.cfg protocol.tla
+```
+
+## Generated PDFs
+
+Typeset versions of the spec are available in [`documents/`](documents/):
+- [`documents/protocol.pdf`](documents/protocol.pdf)
+- [`documents/messages.pdf`](documents/messages.pdf)
+
+PDFs are automatically regenerated by CI on every push to `main` that modifies `.tla` files.
+
+## Configuration
+
+| Constant | Default | Description |
+|---|---|---|
+| `InitialPeers` | `{"peer1", "peer2"}` | Set of peers in the model. Can be extended to more peers. |
+| `MaxBlock` | `3` | Maximum initial block height per peer |