speckl/docs/PROVE-SQLITE-PLAN.md

Prove SQLite — Project Plan

The most deployed database in the world. Never formally verified. We're going to fix that.

---

Objective

Specify SQLite's core state machines in SpeckDL — pager, WAL mode, VDBE bytecode engine, and B-Tree — then verify their critical invariants with Z3. Publish findings. This is the sequel to Prove Kafka (docs/PROVE-KAFKA-PLAN.md, now complete).

---

Why SQLite

SQLite is the most deployed database engine in the world — every smartphone, every browser, countless embedded systems. Its testing infrastructure (TH3, 100% branch coverage, mutation testing) is among the best in the industry. But coverage is not proof.

Formal verification of SQLite's core invariants would be a first. Not a theoretical exercise — this is software running on billions of devices.

---

Phases

Phase 1 — SQLite Pager & Journal Modes

Target: Specify and verify the pager state machine, including transaction lifecycle, journal modes, and WAL concurrency.

Milestone	Description	Dependencies	Status
DB.1	Research doc: pager, WAL, VDBE, B-Tree	None	🚧 In progress
DB.2	SQLitePager.speck	DB.1	⬜
DB.3	Z3 verification of pager invariants	DB.2	⬜
DB.4	SQLiteWAL.speck	DB.1	⬜
DB.5	Z3 verification of WAL concurrency	DB.4	⬜
DB.6	Blog post: "Prove SQLite"	DB.3, DB.5	🚧 In progress

Phase 2 — SQLite VDBE Bytecode Engine

Target: Specify the VDBE execution model — program counter, registers, key opcodes, transaction integration.

Milestone	Description	Dependencies	Status
DB.7	SQLiteVDBE.speck	DB.1	⬜
DB.8	Z3 verification of VDBE invariants	DB.7	⬜
DB.9	B-Tree cursor integration spec	DB.8	⬜

Phase 3 — B-Tree

Target: Specify the B-Tree structure — page organization, splits, merges, cursor operations.

Milestone	Description	Dependencies	Status
DB.10	SQLiteBTree.speck	DB.7	⬜
DB.11	Z3 verification of B-Tree invariants	DB.10	⬜
DB.12	Synthesis: unified SQLite verification report	DB.3, DB.5, DB.8, DB.11	⬜

---

Target Invariants (by layer)

Pager Invariants

1. Transaction atomicity: pages are either fully written or fully rolled back
2. Journal integrity: journal reflects committed state, is cleaned on rollback
3. Cache consistency: dirty pages are written back before journal deletion
4. File format: page size is consistent across the database file

WAL Invariants

1. Read consistency: a reader sees a consistent snapshot (no partial WAL writes)
2. Write serialization: at most one writer at a time
3. Checkpoint safety: checkpoint does not remove frames still needed by active readers
4. Frame ordering: WAL frames are committed in sequence, no gaps

VDBE Invariants

1. Program counter validity: PC stays within instruction bounds
2. Register type safety: read register types match write register types
3. Cursor consistency: open cursors point to valid B-Tree positions
4. HALT guarantee: every program reaches HALT (no infinite loops)

B-Tree Invariants

1. Page organization: every page has valid header and cell pointers
2. Key ordering: keys are sorted within a page and across sibling pages
3. Balance: tree depth is uniform across all leaves
4. Split correctness: splitting a page preserves key ordering and parent linkage

---

Deliverables

• docs/db-sqlite-reference.md — research source material
• examples/SQLitePager.speck — pager + WAL specification
• examples/SQLiteVDBE.speck — VDBE specification
• examples/SQLiteBTree.speck — B-Tree specification
• docs/blog-07-prove-sqlite.md — blog post
• Z3 verification results (sat/unsat per invariant)
• For any gaps found: documented counterexample traces

---

Guiding Principle

Dependencies only. No wall-time estimates. Each milestone lists what must be true before it can start.

Same approach as Prove Kafka, bigger target.