tpt-archon

tpt-archon is a vertically integrated, proof-native computing stack that eliminates the boundaries between storage, operating system, and database. Built inside-out on Rust's ownership model and formal verification, it unifies the page cache, kernel memory management, and database buffer pool into a single, zero-copy address space — see spec.txt for the full design document.

Status

Early but functional across all four layered crates: each phase's core functionality is implemented and tested. A real PostgreSQL wire-protocol server (out-archon-pgwire) sits on top of tpt-archon-relational, so any Postgres client — psql, drivers, ORMs — can talk to Archon directly (see Connect with a Postgres client below); its wire-level behavior is checked against real Postgres by a comparison suite (out-archon-pgcompat, Phase 8 Track C). External verification crates (tpt-eidos-verifier, tpt-telos-*, tpt-gpu-ir-spec, all published to crates.io) are wired in via the non-published crates/out-archon-verify harness, not the shippable crates. GPU support is IR-emission only (no runtime). A real Linux io_uring backend exists behind an opt-in feature (tpt-archon-kernel's io-uring-backend), and a real, cross-platform, read-only mmap zero-copy path exists behind another (mmap, in tpt-archon-core/-bridge/-kernel) — writable mmap and bare-metal driver support are still deferred. Nothing here is production-ready; see TODO.md for the live checklist and what remains (e.g. GPU device execution, mmap backend, publishing).

Phase	Crate	Purpose	Status
1	tpt-archon-core	no_std, zero-allocation storage engine (block device, page manager, WAL, B-Link tree)	Implemented
2	tpt-archon-bridge	Zero-copy IPC & unified page cache traits between storage and kernel	Implemented
2	tpt-archon-kernel	Capability-based microkernel (user-space first) with unified page cache	Implemented
3	tpt-archon-relational	AI-native SQL query engine (GPU opt-in, CPU fallback)	Implemented

The dependency graph is strict and one-directional:

tpt-archon-relational
    ↓
tpt-archon-kernel
    ↓
tpt-archon-bridge
    ↓
tpt-archon-core

TPT ecosystem dependencies

Archon builds on sibling TPT Solutions crates rather than reimplementing verification tooling from scratch:

• tpt-eidos (bare repo; the tpt-eidos-verifier sub-crate) — QF_LRA solver used to prove the B-Link node-capacity / page-fit invariant.
• tpt-telos (tpt-telos-verifier / tpt-telos-ir / tpt-telos-parser sub-crates) — formal verification of critical invariants (WAL crash consistency, MVCC serializability, scheduler deadlock-freedom). There is no standalone tpt-telos crate; those three sub-crates are the package names.
• tpt-gpu (the tpt-gpu-ir-spec sub-crate) — a TPTIR dialect emitter (lowers an IR region to stable TPTIR text). It is not a runtime and does not execute anything. There is no tpt-gpu-primitives or tpt-gpu-runtime crate — they do not exist anywhere in the ecosystem. The GPU path in tpt-archon-relational only emits TPTIR for an external GPU backend; the CPU vector_topk remains the real executor.

These are verification/tooling deps, not runtime deps. None of them are pulled into the shippable crates. They live exclusively in the non-published crates/out-archon-verify harness, as ordinary published crates.io version requirements. See AGENTS.md and ADR 0003.

There is no tpt-zero-bytes crate (referenced in the original design doc but never built anywhere in the ecosystem); the zero-allocation I/O primitives tpt-archon-core needs are implemented directly in that crate instead.

Quick start

The fastest way to try Archon is the interactive SQL shell:

cargo run -p out-archon-sql

This drops you into a REPL where you can create tables, insert data, and run queries:

CREATE TABLE users (id INT, name TEXT, age INT);
INSERT INTO users (id, name, age) VALUES (1, 'alice', 30);
INSERT INTO users (id, name, age) VALUES (2, 'bob', 25);
SELECT name, age FROM users WHERE age >= 25 ORDER BY age;

Or run a single statement non-interactively:

cargo run -p out-archon-sql -e "SELECT 1 + 2;"

No local Rust toolchain? Build and run the REPL in Docker instead:

docker build -t archon-sql .
docker run -it archon-sql

docker-publish.yml also auto-builds and pushes this image to ghcr.io/<org>/<repo>/archon-sql on every v* release tag (and remains available via manual dispatch for an ad hoc build in between releases).

Connect with a Postgres client

Archon also speaks the real PostgreSQL wire protocol, so any Postgres client can connect to it directly instead of going through the archon-sql REPL. Start the server:

cargo run -p out-archon-pgwire --bin archon-pgwire

This listens on 127.0.0.1:5432 by default (override with the HOST/PORT env vars) and accepts unauthenticated (trust) connections. Then, from another terminal:

psql -h 127.0.0.1 -p 5432 -U postgres

Coverage is still narrower than real Postgres — see TODO.md's Phase 8 for what's supported (simple + extended query protocol, SQLSTATE errors, transactions) versus deferred (SCRAM auth, COPY, TLS, pg_catalog emulation).

Which crate should I use?

What you want	Crate	Example
Embed a database in your app	tpt-archon-relational	examples/select_end_to_end.rs
Use the storage engine directly	tpt-archon-core	examples/storage_tour.rs
Run SQL interactively	archon-sql (package out-archon-sql, not published)	cargo run -p out-archon-sql
Connect via psql/Postgres drivers	archon-pgwire (package out-archon-pgwire, not published)	cargo run -p out-archon-pgwire --bin archon-pgwire
Try it in a browser, no install	out-archon-wasm (not published)	crates/out-archon-wasm/www/ — see that crate's README to build/serve it
Use Archon from Python	archon-db (package out-archon-py, PyO3 bindings, not yet on PyPI)	crates/out-archon-py/README.md
Embed the database from Node.js	archon-node (crate out-archon-node, not published to crates.io -- ships to npm)	crates/out-archon-node/README.md
Scaffold a new project	template/	cargo generate --path template
Formal-verification harness	out-archon-verify (not published)	cargo test -p out-archon-verify

Build

cargo build --workspace
cargo test --workspace

License

Licensed under either of:

• MIT License
• Apache License, Version 2.0

at your option.

Contribution

Unless you explicitly state otherwise, any contribution intentionally submitted for inclusion in the work by you, as defined in the Apache-2.0 license, shall be dual-licensed as above, without any additional terms or conditions.