M4.2: TigerBeetle deep verification

agent-engineering commented

2026-05-10 04:42:55 +00:00

What

Extend the existing TigerBeetle spec to full verification, including two-phase commit and overdraft protection.

Tasks

Add two-phase commit state machine to TigerBeetleLedger.speck
Add balance invariants: "no account goes negative" under all failure modes
Add transfer idempotency invariant
Run Z3 verification and document results
Compile to Rust (#25) and benchmark vs TigerBeetle reference implementation
Draft blog post: "We proved TigerBeetle's invariants with Speckl"

Exit Criteria

Full TigerBeetle spec passes Z3 verification
"No negative balance" invariant proven under bounded model checking
Performance comparison with TigerBeetle reference documented
Blog post drafted

Dependencies

#21 (M0.3: Z3 backend) and #25 (M2.1: Rust backend) must be complete.

Context

Part of M4.2 in docs/PROVE-KAFKA-PLAN.md.

## What Extend the existing TigerBeetle spec to full verification, including two-phase commit and overdraft protection. ## Tasks - Add two-phase commit state machine to TigerBeetleLedger.speck - Add balance invariants: "no account goes negative" under all failure modes - Add transfer idempotency invariant - Run Z3 verification and document results - Compile to Rust (#25) and benchmark vs TigerBeetle reference implementation - Draft blog post: "We proved TigerBeetle's invariants with Speckl" ## Exit Criteria - Full TigerBeetle spec passes Z3 verification - "No negative balance" invariant proven under bounded model checking - Performance comparison with TigerBeetle reference documented - Blog post drafted ## Dependencies #21 (M0.3: Z3 backend) and #25 (M2.1: Rust backend) must be complete. ## Context Part of M4.2 in `docs/PROVE-KAFKA-PLAN.md`.

agent-cos referenced this issue

2026-05-10 04:43:02 +00:00

Prove Kafka — Project Plan #17

sscoble commented

2026-05-25 22:28:44 +00:00

Owner

TigerBeetleLedger.speck (155 lines) and TwoPhaseCommit.speck (97 lines) already exist. TigerBeetle spec covers accounts/transfers state machine, balance invariants, overdraft protection, and two-phase commit integration with 3 verify blocks. The ticket's scope (two-phase commit + overdraft protection) is already implemented. Consider adding deeper Z3 model checking in a follow-up. Closing as done.