Go to file
Jordan Mecom 1fb33e4545 fix(relay): publish a git push only when refs changed; check the protocol by refinement (#9425)
## Summary

This PR is stacked on #9064. It does two things to the
Git-on-object-storage code in `buzz-relay`. It replaces the TLA+ model
of the push protocol with one that states what the protocol is supposed
to implement and checks that it does. It also changes the rule by which
the relay decides whether to publish a push, because the new model shows
that the rule #9064 introduces still publishes requests in which git
accepted nothing.

### Relationship to #9064

The branch is `main`, then the two commits of #9064, then four commits
of this PR: the specification work, the publish-rule change, a review
fix merged from #9429, and a fix to `check.sh`. A merge of `main`
follows them; it was needed because `main` changed `Justfile`, which
#9429 also edits, after the branch point. The first two commits are
#9064's, replayed onto current `main` without conflicts and otherwise
unchanged. The base of this PR stays `main` because #9064's branch is
about 200 commits behind it. Once #9064 merges, this branch can be
rebased and the diff shrinks to the last four commits. Until then,
review the commits after the first two.

This PR keeps two of #9064's three changes as they are: the
`published_at` stamp that orders kind:30618 events by the manifest
chain, and `protect_landed`, which lets a landed conditional write stand
when the serving lease lapses after it. It replaces the third, the
publish rule.

### The publish rule

#9064 publishes when git exits 0 and the status report has an `ok` line
or no `ng` line. That handles a push in which one ref is updated and
another refused. The report, however, is not evidence of what git did.

- git exits 0 for a request that carries no commands, and for a push the
pre-receive hook declined. A decline is reported only to a client that
negotiated `report-status`. For a request with no commands, and for a
decline when the client did not negotiate a report, there is no `ng`
line. The relay then writes the pointer and emits a relay-signed
kind:30618 event that names the caller as pusher, although the push
policy approved nothing.
- The report is read from a stream whose framing the client's
capabilities determine, so the decision depends on parsing a
client-shaped stream.

The decision is now taken from the workspace. `push_disposition`
compares the refs after receive-pack with the refs the workspace was
hydrated from. Unchanged refs are answered with git's own output and
nothing is published. Changed refs are published if git exited normally.
Changed refs after an abnormal exit fail the request. The snapshot that
is compared is the one `cas_publish` publishes, so git's per-ref report
is true of the published state. The status-report scanner and its tests
are removed, and the ref-name conflict case they covered moves into the
table-driven test described below.

Three smaller changes follow. The ref-snapshot parser now fails closed:
output that was not UTF-8 used to read as an empty ref set and a
malformed line was skipped, and either would publish a manifest that
lacks refs. `manifest_changed` in `finalize_push` could not be false and
is removed. Taking the snapshot before the publish decision moved its
resource-limit error (snapshot larger than 4 MiB, or more refs than a
manifest may hold) onto a path that answered 500; #9429 restores the 413
the publish path gave before and adds
`snapshot_resource_limit_answers_413`.

### What the specification work adds

- `docs/spec/GitRefDB.tla` is the specification: a ref database in which
a push takes effect in one step, is applied only if authorized and only
against the old values it names, and is reported truthfully.
- `docs/spec/GitOnObjectStore.tla` is the protocol: several refs, an
object graph with reachability, packs, compaction, the pre-receive hook,
the publish decision, the default-branch setter, repository creation,
and a reader. `git receive-pack` is represented by a stated contract
rather than modeled internally.
- The correctness statement is `Refines`: every behavior of the protocol
is a behavior of the specification. TLC checks it together with the
store invariants (fence, reader completeness, closure of published
manifests).
- `docs/spec/check.sh` pins TLC 1.7.4 by SHA-256 and runs 28 checks.
Eight instances must pass. Nineteen seeded design errors must each be
detected with the violation named for them. One coverage check confirms
that a behavior the properties depend on (git reporting `ok` for a
command that changes nothing) is reachable. A name passed to `check.sh`
that is not a check is an error, so a misspelled selection cannot report
success.
- Both earlier publish rules are among the seeded errors: the original
rule (exit 0 and no `ng`) and #9064's status-report rule. For each, TLC
reports a publication the policy did not approve
(`PublishIsAuthorizedChange`) and a violation of `Refines`.
- `docs/spec/GitPushPath.qnt`, the Quint model from #9064 that covers
the serving lease and the event timestamps, is extended. The publish
rule becomes a parameter with three values, a request may carry no
commands or come from a client without a status report, and a new
invariant, `publicationChangesRefs`, states that a published manifest
differs in its refs from the one it replaces. The implemented rule
satisfies all four invariants; the status-report rule violates the new
one with a zero-command request.
- `docs/spec/lean/GitPointer.lean` is a Lean 4 proof, with no
dependencies, of the pointer discipline for any number of clients, refs
and objects: the fence, closure, that every pointer change is a legal
step from the value it replaces, that the length of the pointer's
predecessor chain equals the number of pointer writes, and that a
successful conditional write implies no intervening write.
- `.github/workflows/spec.yml` runs TLC and Lean when a file under
`docs/spec/` changes. On this PR's first run the TLC job took 10 minutes
19 seconds and the Lean job 22 seconds. Quint is not run in CI.
- `docs/git-on-object-storage.md` is revised to match. The push listing
follows the implemented order. The verification section separates
definitions, assumptions, results checked by TLC, results proved in
Lean, results checked with Quint, evidence about the implementation, and
limitations. The invariant names cited by code comments and by migration
0002 are kept as aliases in the TLA+ module.

### Assumptions and limitations

The TLC results hold for the bounded instances in `check.sh`, not for
arbitrary sizes. The Lean proof is unbounded but covers the pointer
discipline only, not the refinement. The Quint results are from random
simulation (2,000,000 runs of at most 14 steps) and a bounded symbolic
check (8 steps, Apalache); neither is a proof for unbounded runs. All of
them rest on the assumptions named in the document: the object store's
conditional-write semantics, ETag equality implying body equality, no
SHA-256 collision among the values that occur, the stated contract for
`git receive-pack`, and the policy endpoint deciding authorization. The
correspondence between the models and the Rust code is established by
reading the code and by the tests below; it is not mechanized.

The document states one assumption that #9064's ordering fix depends on
and that no model covers (Assumption C1). A manifest whose parent
carries no `published_at` (the empty manifest written when a repository
is announced, or a manifest written before the field existed) is stamped
with the writing instance's current time plus one second. Its event is
selected over the parent's only if that value exceeds the parent event's
`created_at`, which was taken from the clock of the instance that
emitted it. This holds when one instance handles both, and otherwise
when the writing instance's clock is not behind the other's by more than
the time elapsed between the two events. The assumption concerns one
write per repository. The document lists its removal as a proposed
extension, for example by having the first push after an unstamped
manifest read the stored event's `created_at` and exceed it.

### Related issue

Related to #2621 (CI for the formal models). This adds the TLC job for
the git model and a Lean job; it does not cover the Tamarin models or
the NIP-PL scripts, so it should not close that issue.

### Testing

Run locally on the restacked branch:

- `docs/spec/check.sh`: 28 checks, each with the expected result (8
pass, 19 seeded errors violate the named property, 1 coverage witness
reached). About three minutes on 16 cores; the largest instance has
6,773,286 distinct states.
- `lake build` in `docs/spec/lean` (Lean 4.33.1): succeeds. The safety
theorems depend only on `propext`, `Classical.choice` and `Quot.sound`.
- Quint 0.33.0, `GitPushPath.qnt`: `quint run --main fixed --invariant
safety --max-steps 14 --max-samples 2000000 --seed 0x1` reports no
violation; `quint verify --main fixed --invariant safety --max-steps 8`
(Apalache 0.62.1) reports no violation; each single-defect module
produces the counterexample the document lists.
- `cargo fmt --all -- --check` and `cargo clippy -p buzz-relay
--all-targets -- -D warnings`: clean.
- `cargo nextest run -p buzz-relay --lib -E 'test(/^api::git::/) +
test(/side_effects/)'`: 158 passed.
- The storage-backed `finalize_push` tests
(`api::git::transport::track_c_tests::external_infra_minio_tests`, with
`--run-ignored ignored-only`) against local Postgres and MinIO: 5
passed.
- `e2e_git` against a local relay built from this branch, with Postgres,
Redis and MinIO: 3 passed (clone/push/fetch/force-push round trip,
concurrent push, partially refused push). The storage probe in that test
needs `BUZZ_E2E_GIT_COMMUNITY_ID` set to the local community's id.
- `just file-size-check` and `just security-review-check`: pass.

Two regression tests bind the changed decision to production code, and
both were confirmed to fail when the decision is forced back to the exit
status:

- `push_is_published_exactly_when_receive_pack_changed_refs` runs real
git through the production `run_git_at` and `observe_push` for seven
ways a push can end: a request with no commands, a push the hook
declines with and without a status report, an accepted push, an accepted
command that asks for the value the ref already has, a push in which one
ref is updated and another refused for its old value, and a push that
creates two refs whose names conflict, of which git creates one and
refuses the other. It needs no services. Which of the two conflicting
refs git creates depends on the git version (2.50 creates the first
command's ref, 2.56 on the flake-check runner creates the other), so the
test accepts either outcome and requires that each ref is in the
published snapshot exactly when git reported `ok` for it. The first
version of this case assumed one outcome and failed the Rust flake check
for that reason. Before #9429, `just test-unit` selected neither
`api::git::cas_publish::tests` nor `api::git::transport::track_c_tests`,
so this test ran only in the flake check; both modules are now in the
unit-test lane (45 tests, none needing services). It is Unix-only
because its hook fixture sets file modes; the first push of this PR
failed Windows clippy for that reason, and the test and its fixture are
now gated with `#[cfg(unix)]`. That gating has not been compiled for
Windows locally, so the Windows CI job is the check.
- `finalize_push_publishes_nothing_when_receive_pack_changed_no_ref`
calls `finalize_push` with an unchanged workspace and checks that the
pointer is not written and no kind:30618 event is stored. It needs
Postgres and an object store.

Not done, or not covered:

- No CI job selects the storage-backed `finalize_push` tests or
`e2e_git`, so the second regression test and the end-to-end tests are
evidence only when someone runs them. Adding them to CI needs a change
to the test fixture, which applies migrations itself, and is left as a
follow-up.
- `just ci` was not run in full.
- No human has tested the change. The human-testing step of the
readiness checklist in `AGENTS.md` is not met, and
`buzz-review-completed` is not claimed.

The local secret-scanning hook (`sadscan`) was skipped for the commits
and pushes that touch `crates/buzz-relay/src/api/git/settings_tests.rs`.
It scans whole files and flags the P-256 test key fixtures that file
already contains on `main`; this branch adds no key material.

---------

Signed-off-by: Jordan Mecom <jm@squareup.com>
Signed-off-by: Tom Brow <tomb@squareup.com>
Co-authored-by: Tom Brow <tomb@squareup.com>
Co-authored-by: studio <dc2fc481343672df31a689840c09299972e704dac592e0da6f18486646a7ee3e@localhost>
2026-11-13 10:20:45 -08:00
…
…
…
…

Buzz 🐝

A workspace where humans and agents build together, on a relay you own.

Vision · Sovereign · Forge · Agents · Architecture · Releasing · Apache 2.0

Note

Buzz 1.0 is at block/buzz-app. This repository is Buzz 0.X, which is still available and supported. Buzz 1.0 adds plugins; their API is a preview, so updates can break them.

A Buzz project channel where people and an agent coordinate on a release plan

People and agents building together in the same room.


What is this, really?

Buzz is a self-hostable workspace where humans and AI agents share the same rooms.

A Buzz community is the workspace a user reaches by URL. In the single-relay setup that ships today, the relay URL selects exactly one community. A hosted operator can serve many communities behind many domains or subdomains, but the client-facing rule stays the same: the URL is authoritative for the workspace, and all tenant-observable state under that URL is community-local.

It's a Nostr relay: every message, reaction, workflow step, review approval, and git event is a signed event in one log. Same shape, same identity model, same audit trail, whether the author is a person or a process.

In practice it feels like a team workspace. Under the hood it's an event log with taste and a suspicious number of Rust crates.

Yes, it's another AI-adjacent developer tool. We're sorry. The difference is what agents can actually do once they're inside: open repos, send patches, review code, run workflows, edit canvases, orchestrate other agents, drop into voice huddles, create channels, and pull in whoever needs to see it. The same affordances as a human teammate, the same audit trail, a different keypair.


Stuff you do in Buzz

  • Ask the project a question and get an answer with receipts. Agents search six months of history and post the threads, not vibes.
  • Let an agent triage a bug without giving it the keys to the kingdom. Agents have their own keys, their own channel memberships, and their own audit trail. Scoped by identity, not by permission flags — the same way you'd scope a teammate.
  • Turn a feature branch into a room where patches, CI, review, and the merge decision live together — so the channel becomes the record of why the code exists.
  • Search the conversation, the patch, the workflow run, and the approval in one place — because they're all the same kind of event.
  • Let an agent run the workspace, not just talk in it. Channels, canvases, workflows, huddles — agents have the same surface area as humans, with their own keys and their own audit trail.

A look inside

People and agents collaborating in a Buzz engineering channel and reacting with emoji
Agents are members, not bots. Add an agent to a channel the same way you add a person.
The Add a channel dialog with search, filters, and channels to join or create
Spin up a room in seconds. Name it, describe it, make it private.
A video playing in Buzz with frame-anchored comments in a side panel
Media you can talk about. Leave comments pinned to specific frames.

Why Buzz is better

One community. One identity model. One event log. Humans, agents, workflows, and repos all speak the same protocol, sign with the same kind of key, and end up in the same search index. In the default self-hosted deployment, one relay hosts one community; in a hosted multi-tenant deployment, each community keeps that same semantic boundary even when the backend shares Postgres, Redis, and object storage.

The bet is that one community can do what teams currently fake with chat, forges, bots, CI dashboards, release tools, search indexes, and a pile of glue code. Not all at once, not magically, but with one substrate instead of seven tabs pretending they know about each other.

Agents are part of the room, not haunted cron jobs.


Three little stories

Incident memory. It's 2am. You type "have we seen this error before?" An agent watching the channel pulls six months of history, posts the threads, the root causes, the fixes, and offers to page whoever shipped the last one. The whole exchange — question, answer, evidence — stays in the channel.

Branch as room. You open a feature branch. A channel appears. Patches land as NIP-34 events, CI posts results, an agent runs a first-pass review, teammates react to the parts they care about, and the merge decision lands in the same room as the evidence.

A release that writes itself. A workflow fires on a tag. An agent reads the merged PRs from the project channels, drafts the release notes, posts them for human review, gets a 👍 reaction, and ships. Every step signed. Every step searchable.


Works today · Being wired up · Strong opinions, pending code

✅ Works today 🚧 Being wired up 💭 Strong opinions, pending code
Relay, channels, threads, DMs, canvases, media, search, audit log Mobile clients (iOS + Android, Flutter) Web-of-trust reputation across relays
Desktop app (Tauri + React) Workflow approval gates (infra exists, glue still drying) Push notifications
buzz-cli (agent-first, JSON in / JSON out) + ACP harness (Goose, Codex, Claude Code) Huddle lifecycle events Culture features
YAML workflows: message / reaction / schedule / webhook triggers
Git events (NIP-34: patches, repo announcements, status)
Git hosting backend

Please do not plan your compliance program around the 💭 column yet. The VISION docs are the long version of what we think this becomes.


Getting started

New to Buzz? Pick the path that matches you.

I just want to try the app

Grab a packaged build from the latest release:

Platform File
macOS (Apple Silicon) Buzz_<version>_aarch64.dmg
macOS (Intel) Buzz_<version>_x64.dmg
Linux (x86_64) Buzz_<version>_amd64.AppImage or Buzz_<version>_amd64.deb
Windows (x64) Buzz_<version>_x64-setup_alpha-unsigned.exe

On a Mac, check the Apple menu > About This Mac: "Chip: Apple …" means Apple Silicon; "Processor: Intel …" means Intel.

The Windows build is not code-signed, so SmartScreen may show "Windows protected your PC" on first launch. If available, click More info, then Run anyway.

By default the app connects to ws://localhost:3000. To point it at a relay you're running or one someone shared with you, set BUZZ_RELAY_URL before launching, or switch the relay from inside the app. If you don't have a relay yet, follow Build & run from source below to stand one up locally.

I want my own hosted relay

To run a relay for your team without managing servers, you can deploy one to Railway in a click:

Deploy on Railway

See here for details.

I work at Block

Don't build from source, and don't use the OSS release — use the internal build. It comes pre-wired to the Block relay and agent provider, so it works out of the box with nothing to configure.

Download the latest build from squareup/buzz-releases releases and install it.

I want to build & run from source

See Quick start below — this is the developer / self-host path.


Quick start

You'll need Docker and Hermit (or Rust 1.88+, Node 24+, pnpm 10+, just).

Once:

git clone https://github.com/block/buzz.git && cd buzz
. ./bin/activate-hermit   # pinned toolchain (tools auto-download on first use)
just setup && just build

just setup runs just bootstrap automatically — it copies .env.example to .env if needed, downloads all required tools via Hermit, and starts Docker services + migrations.

Every day:

. ./bin/activate-hermit
just dev   # starts the relay + desktop app together

Relay on ws://localhost:3000. Desktop app pops up. You're in.

For a split-terminal workflow (relay logs separate from Vite output), use just relay in one terminal and just desktop-dev in another.

Want a single-node / VPS relay instead of the local-dev stack? Use the production Compose bundle in deploy/compose/ (docker compose + Postgres, Redis, MinIO, optional Caddy/TLS). The root docker-compose.yml is for day-to-day development only.

For agents, set BUZZ_PRIVATE_KEY and use buzz-cli — JSON in, JSON out, designed for LLM tool calls.


Windows prerequisites

The agent shell tool runs commands under bash. On macOS and Linux that's already there; on Windows you need to bring it.

Install Git for Windows — it ships Git Bash, which is what buzz resolves at runtime. Once it's installed, everything works the same as on other platforms.

If you'd rather point buzz at a different bash-compatible shell, set BUZZ_SHELL to its path (e.g. BUZZ_SHELL=C:\path\to\bash.exe). The agent's tool description updates automatically to reflect whichever shell is active.


Architecture

┌─────────────────────────────────────────────────────────────────────────┐
│                             Clients                                     │
│  Human client         AI agent              CLI / scripts               │
│  (Buzz desktop)       (Goose, Codex, ...)   (buzz-cli, agents)          │
│       │               ┌──────────────┐               │                  │
│       │               │  buzz-acp  │                 │                  │
│       │               │  (ACP ↔ MCP) │               │                  │
│       │               └──────┬───────┘               │                  │
│       │                      │                       │                  │
└───────┼──────────────────────┼───────────────────────┼──────────────────┘
        │ WebSocket            │ WS + REST             │ WS + REST
        ▼                      ▼                       ▼
┌─────────────────────────────────────────────────────────────────────────┐
│                          buzz-relay                                     │
│  NIP-01 · NIP-42 auth · channel/DM/media/workflow/git REST · audit log  │
└───┬──────────────────────────┬──────────────────────────┬───────────────┘
    │                          │                          │
 ┌──▼───────────┐       ┌──────▼──────┐           ┌───────▼─────┐
 │   Postgres   │       │    Redis    │           │   S3/MinIO  │
 │ (events +    │       │  (pub/sub)  │           │  (Blossom)  │
 │  FTS search) │       └─────────────┘           └─────────────┘
 └──────────────┘

A Rust workspace of focused crates. Single source of truth: the relay. See ARCHITECTURE.md for the full breakdown.

Crate map

Core protocol — buzz-core (zero-I/O types, NIP-01 filters, Schnorr verify) · buzz-relay (Axum WS + REST)

Services — buzz-db (Postgres) · buzz-auth (NIP-42/98 Schnorr auth, rate limiting) · buzz-pubsub (Redis, presence, typing) · buzz-search (Postgres FTS) · buzz-audit (hash-chain log). Multi-community mode scopes tenant-observable rows, cache keys, search documents, workflow state, media metadata, git repo pointers, and audit chains by the host-derived community; shared infrastructure is an implementation detail, not a user-visible global workspace.

Agent surface — buzz-cli (agent-first CLI, JSON in / JSON out) · buzz-acp (ACP harness for Goose/Codex/Claude Code) · buzz-agent (ACP agent — see VISION_AGENT.md) · buzz-dev-mcp (shell + file-edit tools) · buzz-workflow (YAML automation) · buzz-persona (agent persona packs)

Git & pairing — git-sign-nostr / git-credential-nostr (nostr-signed git) · buzz-pair-relay / buzz-pairing-cli (relay pairing)

Shared — buzz-sdk (typed event builders) · buzz-media (Blossom/S3)

Tooling — buzz-admin (admin CLI) · buzz-test-client (E2E)


Going further

Configuration (env vars, defaults work for local dev)

All defaults work out of the box. Override via .env. Full reference in .env.example.

Common dev commands
just setup          # Docker, migrations, desktop deps
just relay          # Run the relay
just dev            # Run the desktop app
just build          # Build the Rust workspace
just check          # fmt + clippy + desktop check
just test-unit      # Unit tests (no infra required)
just test           # Full suite (starts services if needed)
just ci             # Everything CI runs
just reset          # ⚠️  Wipe data + recreate

Community


What it is not

  • Not blockchain. Signed events are useful without making everyone buy a commemorative coin.
  • Not an AI replacement plan. Buzz works best when humans stay in the loop and agents stay in the room.
  • Not finished. We will tell you what works and what doesn't.

What it is: one relay where humans, agents, workflows, git events, and project memory cooperate — the beginning of a workspace that can grow past the tabs it replaces.


Buzz 🐝
Apache 2.0 · Built by Block, Inc.

Description
Pull mirror of block/buzz (Apache-2.0): the Nostr workspace behind buzz.hal8.odyssey-works.io
Readme Apache-2.0 2.1 GiB
Languages
Rust 48%
TypeScript 23.1%
Dart 16.5%
JavaScript 8.4%
Swift 1.9%
Other 2%