WORK IN PROGRESS — pre-mainnet, private testnet only

SQL on a post-quantum blockchain

The web3 backend for SQL-based applications. 99% of websites that matter run on SQL. Seal gives them decentralization, privacy, and post-quantum security — without changing how they work.

Status: Seal DAO is a research and engineering project under active development. No token has been issued. No rewards, grants, airdrops, or bounties are being paid or promised. Any economic parameters described on this site are design sketches, not commitments. Everything is subject to change.

# Deploy your app
seal app deploy --name myapp.seal --schema schema.sql

# Query from anywhere
seal sql "SELECT * FROM myapp.users" --node http://node:8545

# Your schema.sql is just PostgreSQL
CREATE TABLE users (
  id BIGINT PRIMARY KEY,
  email TEXT NOT NULL,
  balance BIGINT DEFAULT 0
);

Get Started GitHub

Post-Quantum Crypto

ML-DSA-65, ML-KEM-768, SHA3-256. NIST-standardized. Future-proof against quantum computers. No classical crypto on-chain.

PostgreSQL-Compatible SQL

CREATE TABLE, INSERT, SELECT, JOIN, WHERE. Row-level security with CREATE POLICY. Your existing SQL skills work here.

Three Privacy Levels

Public tables, RLS-protected tables, and private tables encrypted at rest. MPC aggregates and ZK proofs for private data access.

Namespace Sharding

Each app gets its own shard. Nodes choose which namespaces to serve. Scales horizontally as the network grows.

Verifiable Queries

Every query result is backed by a Merkle proof against the state root. ZK proofs via RISC Zero / SP1 for privacy-preserving verification.

On-Chain DEX

Built-in limit order book. Create custom tokens, trading pairs, and place orders. All signed with ML-DSA-65.

What Seal adds to SQL websites

Today	With Seal
You manage your own database servers	The network manages replication for you
You build auth from scratch	Cryptographic identity built-in (ML-DSA)
You trust your hosting provider with your data	Data encrypted at rest, verified by math
You hope your backups work	Replication across multiple nodes by default
Users trust you not to tamper with data	Merkle proofs and ZK proofs verify everything
Vulnerable to quantum computers (eventually)	Post-quantum from day one (ML-DSA, ML-KEM, SHA3)
Locked to a cloud vendor	Decentralized, no single point of failure

Wallet & Tools

All signing with ML-DSA-65 post-quantum signatures. SQL, tokens, DEX, MPC, ZK proofs.

Desktop Wallet — SQL queries

Desktop wallet: wallet, node connection, SQL query results

MPC Aggregates & ZK Proofs

MPC sum aggregate and ZK proof generation

Tokens & DEX Order Book

Token creation, minting, DEX limit order book with depth visualization

TUI Wallet — Terminal

TUI wallet: restore, connect, place order, colored order book

Network status

887

Tests passing

66

Kani proofs

9

Fuzz targets

19

Crates

Quick Start

Build from source

git clone https://github.com/SealProjectDAO/seal-dao-public.git
cd seal-dao-master
cargo build --release -p seal-node -p seal-cli

Start a node

./target/release/seal-node --slots 0 --rpc-port 8545

Runs forever, serves JSON-RPC on port 8545.

Query via CLI

seal-cli sql "SELECT * FROM users" --node http://localhost:8545
seal-cli sql "INSERT INTO users VALUES (3, 'charlie', 750)" --node http://localhost:8545

Query via curl

curl -s localhost:8545 -H "Content-Type: application/json" \
  -d '{"jsonrpc":"2.0","method":"seal_querySql",
       "params":{"sql":"SELECT * FROM users"},"id":1}'

RPC API

Method	Auth	Description
`seal_querySql`	No	Execute a read-only SQL query
`seal_submitSql`	ML-DSA	Submit a write (INSERT/UPDATE/DELETE/CREATE)
`seal_getHeight`	No	Get current block height
`seal_getStateRoot`	No	Get current state root hash
`seal_getBlock`	No	Get block by height
`seal_deployNamespace`	ML-DSA	Deploy a new app namespace
`seal_createToken`	ML-DSA	Create a custom token
`seal_mintToken`	ML-DSA	Mint tokens to an address
`seal_createPair`	ML-DSA	Create a DEX trading pair
`seal_placeOrder`	ML-DSA	Place a limit order (bid/ask)
`seal_getOrderBook`	No	View order book depth
`seal_mpcAggregate`	Optional	Run MPC aggregate on private data
`seal_zkProve`	Optional	Generate ZK proof (RISC Zero / SP1)

SQL Reference

PostgreSQL-compatible subset. Your existing SQL works.

Supported

CREATE TABLE, DROP TABLE
INSERT, UPDATE, DELETE
SELECT with WHERE, ORDER BY, LIMIT
JOIN (INNER, LEFT)
BIGINT, TEXT, BOOLEAN
PRIMARY KEY, NOT NULL, DEFAULT
CREATE POLICY (RLS)
CREATE NAMESPACE

Coming soon

ALTER TABLE
CREATE INDEX
Subqueries
Aggregate functions (SUM, AVG, COUNT)
  via MPC for private tables
GROUP BY, HAVING
Foreign keys
Views

Run a Validator

Algorand-style consensus: VRF leader election + committee voting. No mining, no GPUs.

Requirement	Minimum	Recommended
CPU	4 cores	8 cores
RAM	16 GB	32 GB
Storage	500 GB NVMe	1 TB NVMe
Network	100 Mbps	1 Gbps
Stake	TBD — no token is issued and no stake is currently required

Setup

# Build
cargo build --release -p seal-node

# Start validator
./target/release/seal-node --slots 0 --port 4001 --rpc-port 8545 \
  --bootstrap-peers /dns4/boot1.seal-dao.network/tcp/4001

Economics (design sketch — not implemented)

The parameters below are provisional design notes. No token has been issued, no rewards are paid, no slashing is active, and nothing here constitutes a commitment or an offer.

Block Rewards (design)

Target emission curve under study. Exact numbers, recipients, and mechanism are not finalized and may never be deployed as described.

Fee Revenue (design)

Dynamic-fee model under study. No fees are collected today and none are being distributed.

Slashing (design)

Slashing and unbonding mechanics are specified but not yet active in any production setting.

Three-Body Governance (design sketch — not active)

The governance structure below is a specification. No token has been issued, no treasury exists, and no grant or treasury-spend process is live or planned to go live on any particular date.

Token House (future)

In the designed model, SEAL token holders would vote on proposals with conviction voting and delegation caps. No token is issued today.

Technical Council

7-11 members. Whitelist emergency proposals, veto dangerous changes. Term-limited. Not yet seated.

Service Operators

Active validators. Advisory endorsement on operational proposals. SLA-based veto power. No live network yet.

Proposal Tracks (design sketch)

Design thresholds only. Governance is not active; no proposals are live; nothing on this table authorizes spending of any funds.

Track	Approval	Quorum	Timelock
Runtime Upgrade	75%	50%	7 days
Parameter Change	66%	33%	2 days
Emergency	90%	67%	None
Text / Signal	50%	10%	None

Documentation

WORK IN PROGRESS

Formal Verification

Tool	What it proves	Status
Lean 4	Merkle tree invariants, VRF uniqueness	0 sorries
Rocq/Coq	Token conservation, RLS non-bypass, SQL transitions	0 Admitted
Kani	Overflow, bounds, arithmetic (66 harnesses across seal-token / consensus / merkle / crypto / threshold / node / bridge)	66/66 pass
Miri	Undefined behavior detection	Pass
cargo-fuzz	Crash-free on random input (9 targets)	0 crashes
TLA+	Consensus safety and liveness	Spec + trace

Crate Map

Crate	Purpose
`seal-crypto`	ML-DSA, ML-KEM, SHA3, address derivation
`seal-vrf`	PQ-VRF (ML-DSA + SHA3), LaV many-time VRF, LB-VRF placeholder
`seal-threshold`	Ringtail lattice threshold signatures (full protocol), NTT, Shamir
`seal-ringtail-verify`	`no_std` Ringtail verifier for Solana BPF and Stellar Soroban
`seal-consensus`	VRF election, committee voting, fork choice, epochs, slashing
`seal-sql`	SQL parser, engine, RLS, namespaces
`seal-procs`	SQL stored procedures (PL/pgSQL-shaped, ADR-001 default contract model)
`seal-merkle`	Merkle tree, persistent RB-tree indexes (Aeneas-extracted into Lean)
`seal-storage`	Block store, state pruning, HAMT
`seal-token`	Balances, emission, treasury, per-block batch-auction DEX, fees
`seal-p2p`	libp2p GossipSub, mDNS, ML-KEM transport
`seal-zk`	RISC Zero, SP1, GPU acceleration, batch proofs
`seal-mpc`	SPDZ private aggregation, PSI
`seal-tee`	TEE attestation wiring (SGX / SEV-SNP / TDX shapes)
`seal-bridge`	Solana + Stellar bridge observers, per-chain emergency pause
`seal-node`	Node binary, RPC server, disk persistence, bridge RPC wiring
`seal-wallet`	Shared wallet core (ML-DSA-65, BIP-39); Electron / Android / browser-extension shells
`seal-app`	App packaging: `.seal` schemas, deploy, namespace routing
`seal-cli`	CLI: dev, demo, sql, migrate, app deploy

Dev Blog

Engineering notes are posted at zeta1999.github.io/renoir42. Summaries below; follow the titles for the full write-up.

Seal DAO: what landed in the private tree this week (not yet pushed public)

2026-04-21 · ringtail · bridges · demo-apps · adr-001

Field note on the week between the 2026-04-13 public-mirror sync and now. Most of the following is in the private tree; a batched public push is coming once the bridge e2e scripts stop finding their own bugs.

Full Ringtail protocol path (Lagrange coefficients + canonical rounding), replacing the SimpleThreshold signature-list stand-in — the 2-round aggregate shape from ePrint 2024/1113.
seal-ringtail-verify: no_std verifier that compiles for Solana BPF and Stellar Soroban; feature-gated on both bridges. Compute-unit projections in place for the BPF side.
Real Solana/Stellar observer RPC clients; Anchor + Soroban programs for committee-MAC verify; real SAC transfers on Stellar; a docker-compose + bridge-e2e.sh that drives a bridged-asset round-trip locally.
Per-chain bridge emergency pause with a 2/3 Technical Council supermajority gate; seal_getBridgeStatus surfaces paused_chains.
TxType::DexMatch emitted per block, so matched trades land in the state root and ZK proof rather than only in the engine's in-memory book.
ADR-001: SQL stored procedures (CALL / PL/pgSQL-shaped) as the default contract model, WASM as an opt-in path with wasm-validate at deploy.
Four demo apps under apps/: copy-trading.seal, kyc.seal, kindle.seal, forms.seal (MPC + ZK + AEAD + browser wallet end-to-end).
Kani 66/66 (the last 6 closed by a BTreeMap swap + harness refactor); test count 820 → 887 over the week.

Seal DAO architecture: what the 17 crates actually do today (updated, WIP)

2026-04-12 · architecture · consensus · sql

Against the current tree, crate by crate — what's wired, what's a placeholder with a TODO header, and what's honestly aspirational. Corrections vs. an earlier draft: production sortition is ML-DSA + SHA3 (not "Algorand VRF"); SimpleThreshold is a signature-list stand-in and RingtailThreshold is the real one; the DEX is a per-block batch auction with Lean-proved matching invariants. Bridges are TLA+-proved on the invariants but not yet production-validated end-to-end against a live Solana / Stellar validator.

Formal verification on Seal DAO: TLA+, Lean 4 + Aeneas, Rocq, Kani (updated)

2026-04-05 · formal-methods · lean · rocq · tla+

Counted against the current formal/ tree: TLA+ (3 specs + 2 model-check drivers; SealConsensus covers Agreement / NoEquivocation / MonotonicHeight / Progress on 2/3-threshold voting; SealBridge maps MintedLeqLocked, NoDoubleMint, NoMintWithoutLock, BurnedLeqMinted to concrete checks in bridge.rs). Lean 4 with an Aeneas MIR-extraction pipeline on seal-merkle, plus hand-written proofs for Hash, VRF (LaV), and DEX matching — 29 theorems. Rocq modules for Balance, StateMachine, SqlState, RLS — 29 theorems. 66 Kani harnesses across 19 files. 9 cargo-fuzz targets. Miri is a soft skip in CI today, which is a known gap.

ML-KEM-768 in rust-secure-memory: what's wired, what isn't (updated)

2026-04-12 · pqc · ml-kem · secure-memory

Adjacent project, same stack. ML-KEM-768 (FIPS 203) is wired as a standalone primitive in rust-secure-memory — 1184-byte public keys, 1088-byte ciphertexts, 32-byte shared secrets. Important correction over an earlier draft: Enclave sealing is symmetric-only (XChaCha20-Poly1305 with a per-process session key), and ML-KEM is not currently in the sealing path. Three Kani harnesses plus a cargo-fuzz target cover input validation and the FIPS 203 implicit-rejection behaviour; neither proves anything about ML-KEM's underlying MLWE/MLWR soundness.

More posts (FPGA meta-compiler, Thetis26 wait-free, Monte Carlo GPU, concurrent C++ verification, ARIA strategy DSL, market-data terminal, LOB reconstruction on GPU, tabular embedding, QML build pipeline, etc.) at zeta1999.github.io/renoir42.

Community

GitHub

Source code, issues, pull requests. 19 crates, 887 tests, formal verification.

Discord

Developer chat, validator coordination, governance discussion. Coming soon

Twitter / X

Announcements, releases, ecosystem updates. Coming soon

Contributing

# Clone and build
git clone https://github.com/SealProjectDAO/seal-dao-public.git
cd seal-dao-master
cargo build && cargo test

# Run the full verification suite
./scripts/ci.sh quick    # build + 887 tests + clippy
./scripts/ci.sh          # + Kani + Miri + fuzz + audit

Seal DAO is pre-mainnet and under active development. Report security issues via a private GitHub security advisory on the repository. No bounty program is in place and none is promised.