image:[License,link="https://github.com/hyperpolymath/palimpsest-license"]

FormDB Debugger

Proof-carrying database debugger for FormDB using Lean 4 and Idris 2.

What is FormDB Debugger?

FormDB Debugger is a verified database troubleshooting and recovery tool. Unlike traditional database debugging tools that rely on intuition and experience, FormDB Debugger generates machine-checked proofs that recovery operations are safe before executing them.

Key Features

• Proof-Carrying Recovery - Every recovery operation comes with a Lean 4 proof of correctness

• Temporal Navigation - Time-travel through database states with provenance tracking

• Constraint Violation Analysis - Trace exactly why constraints failed and how to fix them

• Verified Migrations - Prove that migrations preserve data before running them

• Audit-Grade Documentation - Generate formal verification reports for compliance

Why?

Current database debugging tools have fundamental limitations:

Tool	Problem
EXPLAIN ANALYZE	Read-only, can’t help with recovery
WAL viewers	Raw bytes without semantic understanding
pg_dump/restore	All-or-nothing, no surgical repair
Database GUIs	Visual inspection without verification

When data corruption, failed migrations, or constraint violations occur, administrators rely on hope and experience. There’s no way to prove a recovery operation is safe.

FormDB Debugger changes this by leveraging dependent types and theorem proving to guarantee correctness.

Quick Start

# Clone the repo
git clone https://github.com/hyperpolymath/formdb-debugger

# Build the core library (requires Lean 4)
cd core && lake build

# Build the Idris 2 REPL
cd ../idris && idris2 --build debugger.ipkg

# Build the TUI
cd ../ui && cargo build --release

# Connect to your database
formdb-debug --connect postgres://localhost/mydb

Example Session

formdb-debug> explain violation fk_author_id

Constraint Violation Analysis
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━

Constraint: evidence.author_id REFERENCES authors(id)
Violation:  Row evidence[42] references authors[7] which does not exist

Suggested Fixes:
  [1] Re-insert the deleted author (proof: FK_SATISFIED)
  [2] Update evidence to reference existing author (proof: FK_SATISFIED)
  [3] Delete the orphaned evidence row (proof: CASCADE_SAFE)

formdb-debug> recover 1 --verify

Recovery Plan verified:
  ✓ FK_SATISFIED
  ✓ LOSSLESS
  ✓ REVERSIBLE

Execute? [y/n]: y
✓ Recovery complete

Architecture

formdb-debugger/
├── core/          # Lean 4 proof library
├── idris/         # Idris 2 interactive shell
├── adapters/      # Rust database adapters
└── ui/            # Ratatui terminal UI

See SPEC.adoc for the full specification.

Status

Phase: Specification

This project is in the specification phase. The core proof library and adapters are planned but not yet implemented.

Related Projects

• FormDB - The narrative-first database this debugger supports

• FQLdt - Dependently-typed FormDB Query Language (compile-time proofs)

• FormDB Studio - Zero-friction GUI for non-technical users

• BoFIG - Evidence graph for investigative journalism

• Zotero-FormDB - Reference manager using FormDB

• FormBase - Open-source Airtable alternative with provenance

License

PMPL-1.0-or-later