Tabula

Tabula is a zero-knowledge kernel for typed, tabular state transitions.

Instead of treating application logic as a general-purpose machine trace and then proving that trace, Tabula treats typed state transitions themselves as the thing to execute, validate, and prove. The project is built around the idea that many applications do not naturally think in terms of flat VM memory. They think in terms of structured state, explicit reads and writes, and schema-level meaning. Accounts, balances, orders, permissions, and ledgers are usually closer to tables than to machine memory.

Why This Approach

General-purpose proving systems are powerful, but they flatten structured application logic into machine steps. Once that happens, the system sees less of what actually matters: state shape, read/write structure, and program meaning.

Tabula keeps that structure visible. By working with typed state transitions, it can push more validation, analysis, and proof planning to compile time instead of rediscovering the same facts inside every proof. That is one of the central ways it aims to reduce proving cost.

Core Idea

Tabula is organized around a few durable ideas:

• state lives in typed tables addressed by (table, column, row)
• programs are registered as explicit semantics, not just raw source text
• compile-time analysis is part of the optimization story: work resolved statically is work the prover does not need to pay for repeatedly
• execution, commitment semantics, and proving are separate layers
• tabula-sdk is the default product-facing integration boundary
• tabula-runtime remains the lower-level native orchestration layer
• the proof backend should be replaceable without redefining program meaning

Architecture At A Glance

authoring input
  -> language front-end
  -> IR
  -> semantic registration
  -> runtime execution and policy
  -> proof preparation
  -> proof backend

At the workspace level, the architecture is split into a few clear layers:

• shared meaning: tabula-core, tabula-contract
• authoring and registration: tabula-lang, tabula-ir, tabula-compiler
• execution and runtime policy: tabula-executor, tabula-runtime
• proof backend: tabula-commitment, tabula-witness, tabula-gadgets, tabula-chips, tabula-stark, tabula-machine
• package surfaces: tabula-ext, tabula-sdk, tabula-cli

For the canonical current architecture, read docs/design/architecture.md.

Where To Read Next

• docs/design/architecture.md Cross-crate architecture and dependency direction.
• docs/README.md How to interpret design/, notes/, research/, and archive/.
• crate README.md files under crates/ Crate-local contracts, design intent, and ownership boundaries.

Getting Started

Build and test the workspace:

cargo build
cargo test

Generate example inputs and run a local batch:

cargo run -p tabula-cli -- example basic --dir /tmp/tabula-example
cargo run -p tabula-cli -- execute \
  --program /tmp/tabula-example/program.tab \
  --state /tmp/tabula-example/state.json \
  --batch /tmp/tabula-example/batch.json \
  --context /tmp/tabula-example/context.json

Produce and verify a proof from that execution:

cargo run -p tabula-cli -- execute \
  --program /tmp/tabula-example/program.tab \
  --state /tmp/tabula-example/state.json \
  --batch /tmp/tabula-example/batch.json \
  --context /tmp/tabula-example/context.json \
  --receipt-out /tmp/tabula-example/receipt.bin

cargo run -p tabula-cli -- prove \
  --program /tmp/tabula-example/program.tab \
  --receipt /tmp/tabula-example/receipt.bin \
  --proof-out /tmp/tabula-example/proof.bin \
  --statement-out /tmp/tabula-example/statement.json \
  --summary-out /tmp/tabula-example/proof_summary.json

cargo run -p tabula-cli -- verify \
  --program /tmp/tabula-example/program.tab \
  --proof /tmp/tabula-example/proof.bin

Check, inspect, or compile a .tab program:

cargo run -p tabula-cli -- check path/to/program.tab
cargo run -p tabula-cli -- schema path/to/program.tab
cargo run -p tabula-cli -- compile path/to/program.tab

Project Status

Tabula is still early-stage and the architecture is evolving quickly.

The canonical documentation set therefore tries to optimize for durable boundaries rather than implementation detail:

• the root README.md explains the project and its thesis
• docs/design/architecture.md explains the current cross-crate architecture
• crate README.md files explain local contracts and design intent

Exploratory material and historical documents still exist, but they should not be treated as the primary source of truth for the current workspace.

License

MIT OR Apache-2.0