bide v0.9.0

Correction (2026-10-02). This release's README overstated gsm's convergence guarantee: gsm v0.11.0 could certify some machines as convergent when they aren't (when one event reads a variable another event writes), and the proof-extracted checkers didn't run in Build or CI. The proof is correct; the implementation skipped a precondition. Fixed in gsm#2; details in bide#142.

A claim protocol checked by a model checker, on a core built for 1.0.

v0.9.0 is the release where bide's coordination protocols are checked, not only tested. TLA+ models of claims, approvals, flows, spend and the bide protocol run with the TLC model checker on every pull request, and the engine underneath them is rebuilt around a storage port and a journal with its own format. Model calls are typed values with exact spend accounting, flows run on durable Steps, proofs commit to the bytes the journal stores, and every audit entry point works under any signature scheme.

• The claim protocol, model-checked in CI. TLA+ models (written in PlusCal) cover attempt claims, not-started records, numbered retries, the resume gate and halt resolution (model 1); the approval gate with 1-of-1 and m-of-n tallies and approvers' key sets (model 1b); flow semantics (model 7); spend accounting (model 8); and the bide protocol's claim rules for remote tool calls (model 2). TLC explores every interleaving within each configuration's bounds, and Models is a required check on every pull request. Each counterexample the checker finds becomes a deterministic Go regression test, the Go fault-schedule exploration of concurrent claims is deterministic too (with a nightly full-bound run), and the model's findings are now properties the engine holds: each effect fires at most once, at most one attempt of a call is live, a resolver that never overrides a live driver, and a claim's winner that never halts on a loser's behalf. See spec/tla.
• A Store/Journal core. agent.Store is a small storage port (Insert, Get, Load) with its requirements numbered A1 to A8 on the type, and agent.Journal owns everything above it: memoization, the record encoding and salt, attempt claims, not-started records and recording an outcome after the caller's context ends. Every journal opens with an @journal header naming its format, so a run in another format is refused before anything is read or written. agent/storetest checks any store against every requirement, RunFilter lets SQL stores list only unfinished runs, and a counting store holds the engine to an exact budget of store round trips per operation. Journals in one process share in-flight steps, and a claim whose write may not have committed is recorded as not started, so a re-drive re-attempts the effect rather than halting over one that never ran.
• A sealed pause contract. Every pause satisfies agent.Pause, with five kinds (ApprovalPending, InterruptPending, SignalPending, TimerPending, OutcomeUnknown) and verbs named for the pause they answer (SubmitDecision, AnswerInterrupt, Enqueue). agent.ResolveHaltRef resolves tool and Step halts alike, knows whether a halt was crashed or contended, and refuses to resolve an effect a live driver may still be running.
• Typed model calls and exact spend. A model call is an agent.ModelCall value and returns an agent.ModelResponse, so middleware passes the call on instead of threading engine state through the context, and agent.CallModel sends one outside an agent through the same checks. Hooks are append-only with exactly one After per Before, the spend meter sits beneath every middleware, and requests are numbered across retries and hedged targets. A run that ends waits briefly for requests still in flight and journals their usage as late spend, so hedge losers and abandoned requests count toward Result.Spend, the budget and Replay. Each turn journals its finish reason, the model that answered, and digests of the prompt and tool set it was sent. The stream sink is claimed by one request per turn, so a hedged turn streams live from its first target.
• Flows on durable Steps, with conformance. Every plan node runs as an agent.Step, so flows get the Step's claim protocol, pause guard and halt resolution (plan.Flow.ResolveHalt). A flow run records what it is (RunKindFlow, its name and canonical input) and run:complete when it finishes, so recovery skips finished flows and a later drive returns the recorded output with one point read. Steps inside a loop body are scoped per iteration, and Conform replays a run's routing from its recorded choices. A fault-schedule exploration of the lowering (crashes, store errors and cancellations at every write, across processes) runs as a permanent test.
• Proofs over the bytes the journal stores. A journal leaf is its tag followed by the record's stored bytes (Record.Raw), so a record written by a later release verifies unchanged, and audit.ExportJournal hands an auditor exactly those bytes. Every artifact names its format (proofs v3, evidence v5, STH v5), and audit.UnmarshalStrict checks it at every depth. Projections refuse a journal they cannot represent exactly, with ErrRedacted or ErrMalformed, and verifiers return an error that wraps ErrNotVerified, ErrFormat or ErrMalformed.
• Signature agility and post-quantum hybrid. Every audit entry point takes an audit.Signer or audit.Verifier, so ed25519, ML-DSA-65 (FIPS 204) and the ed25519 plus ML-DSA-65 hybrid work throughout: tree heads, evidence, run certificates, approvals, grants, the standalone audit/verify package and bide-audit. The scheme is part of the signed bytes, keys have one text form (<alg>:<hex>), and each half of a hybrid signature signs its own label, so neither half verifies on its own. An m-of-n decision is journaled with the scheme it was signed under.
• Approval key identity. An approver's verifier reports the identities of its signing keys (KeyIDs), and the m-of-n gate counts one seat per signing key: a policy whose approvers share a key is refused on every evaluation, by the gate, TallyApprovals, audit.VerifyApprovals and bide-audit verify-approvals alike. Ed25519 keys are checked for canonical encoding and full order (audit.CheckEd25519PublicKey), so every accepted key is exactly one key.
• The bide protocol, designed for SDKs. bide.protocol.v1 is the accepted design for using bide from other languages: the Go engine stays the only writer of the journal, claims and proofs, while Python and TypeScript SDKs run tools and answer pauses, as long-lived workers or serverless functions. Its claim rules pass model 2. Implementation follows the engine hardening of the pre-1.0 redesign.
• Postgres stores that hold nothing between round trips, in a schema you pin. Every store/postgres lease call and journal insert, and every govern/postgreslog append, is one statement that Postgres commits before it replies. An insert takes its position from a next_seq plpgsql function under a transaction-level advisory lock that ends with the statement, so a stalled client holds no lock and another node takes a run over one TTL after its last committed renewal. Every name the stores send is qualified: tables and next_seq with the store's schema, and every function, type and operator with pg_catalog (operators as OPERATOR(pg_catalog.<op>)), and a static check holds every statement to that rule. WithSchema pins the schema so the search path plays no part, and pinning it is the recommended setup. Open checks that the tables carry the unique indexes the statements rely on, and that next_seq has the expected definition, owner and search_path.
• Recovery that drives only unfinished runs. Holding a run's lease, Recover and RecoverLoop check its end-of-run markers again before calling resume, so a run finished by another lease holder after the pass listed it is left alone, for three point reads per driven run.
• Performance. On a standard 4-vCPU GitHub runner (AMD EPYC 7763, median of 21, run 36802470752), the overhead scenario runs ~25,400 runs/s at a mean run latency of 10.1 ms (p90 22 ms, p99 50 ms), and 20,000 runs with 5,000 in flight and 50 ms model calls finish in about 1.01 s (~19,900 runs/s, mean 251 ms, p90 321 ms, p99 447 ms). A same-ref run on the same CPU model put the noise within 2.7% on every one of these metrics. Throughput is flat to slightly up against v0.8.0: the Store/Journal core (#92) gained about 10%, and typed model calls (#104) gave back 3 to 8% as Record grew. The fan-out p99 is higher than v0.8.0's (447 vs 419 ms) while throughput and the mean improved: #92's sixth journal record per run (the @journal header) reshapes the latency distribution, and the Record shrink planned after P12 is expected to recover some of it. Latency is reported as the mean, p90 and p99, since the closed-loop harness's p50 is bimodal, sitting on a scheduling cliff (cmd/bench).

API changes:

• Every journal starts with an @journal header (format bide.journal.v1-dev), so History returns it first and record indices shift by one; journals written by v0.8.0 and earlier are refused, not resumed.
• store/sqlite names its tables bide_steps, bide_leases and bide_schema_version, and store/postgres its leases table bide_leases; stop every v0.8.0 node before starting v0.9.0.
• agent.Lister.Runs takes a RunFilter and returns an iterator; agent.Capability takes a Store; Record.Salt and Record.Claim are read through Salt() and ClaimID().
• The pause types are ApprovalPending, InterruptPending, SignalPending, TimerPending and OutcomeUnknown, each embedding RunRef; the old names remain as deprecated aliases. ApproveAs is removed; use SubmitDecision.
• Waker.Schedule returns an error, and ResolveHaltRef (with its wrappers) refuses to resolve an effect a driver may still be running (*HaltInFlight), a conflicting outcome (*HaltAlreadyResolved) and an operation that never halted (ErrNoLiveAttempt).
• A Step that is not retry-safe and returns a pause is ErrConfig; step names must be non-empty, and node:, switch: and flow: are reserved prefixes.
• plan nodes are journaled as Steps under node:<name> (node:iter:<n>:<name> in a loop), a flow records run:start and run:complete, flow inputs compare as canonical JSON, and plan.HaltAmbiguous is removed; flows started under v0.8.0 do not resume.
• agent.ModelHandler is func(ctx, ModelCall) (ModelResponse, error), hooks are added with ModelCall.AddHook, and DetachModelSink, EmitMessage, WithModel(ctx, m) and WithModelCallHook(ctx, h) are removed.
• Spend records are keyed @spend/<id>, agent.Finish needs keyed literals, and an empty finish reason is recorded as stop.
• middleware.CostMeter reports through Snapshot(); trace.WithSystem and trace.WithModel are removed.
• Proofs carry RecordBytes instead of Record, artifact formats move to proof v3, evidence v5 and STH v5 (re-create older artifacts from the journal), and TreeHead.Timestamp is TimestampNanos.
• Audit signing and verification take an audit.Signer or audit.Verifier, verifiers return error, EvidencePackage names its key as {alg, public_key}, and NewAuditedStore returns an error.
• agent.ApproverVerifier has Alg() and KeyIDs(), and SubmitDecision requires Decision.Alg.
• Grant.NotAfter is NotAfterUnix, stream and model event JSON is snake_case, and audit.PoliciesUsed, audit.AbsenceRoot and audit.KeyFunc return errors or key lists.
• bide-audit reads keys as <alg>:<hex> and journals as a JournalExport.
• The Postgres stores' Open refuses existing tables without the unique indexes their statements rely on, and a next_seq function with another definition, owner or search_path.

Journal format and upgrades: every pre-release, v0.9.0 included, writes the one format tag bide.journal.v1-dev. From known limitations: "Before 1.0, a run is not promised to resume across releases. Every pre-release writes the same journal format tag, bide.journal.v1-dev, and the tag is not bumped when the keys or the record shape change between pre-releases, so a later pre-release does not refuse an earlier one's journal even where it reads it differently. Finish or resolve runs before upgrading between pre-releases. At 1.0 the tag becomes bide.journal.v1, and 1.0 refuses every pre-release journal." Upgrading from v0.8.0 is not a rolling deploy: finish or resolve its runs, stop every v0.8.0 node, then start v0.9.0. On Postgres, pin the store's schema with WithSchema.

Install:

go get github.com/bide-ai/bide@v0.9.0

Library modules, at the same version:

go get github.com/bide-ai/bide/store/sqlite@v0.9.0
go get github.com/bide-ai/bide/store/postgres@v0.9.0
go get github.com/bide-ai/bide/mcp@v0.9.0
go get github.com/bide-ai/bide/trace@v0.9.0
go get github.com/bide-ai/bide/codec/gcf@v0.9.0
go get github.com/bide-ai/bide/govern@v0.9.0
go get github.com/bide-ai/bide/govern/sqlitelog@v0.9.0
go get github.com/bide-ai/bide/govern/redislog@v0.9.0
go get github.com/bide-ai/bide/govern/postgreslog@v0.9.0

Docs: https://bide-ai.com. Formal models: spec/tla.