Published, pending, and how to ask.
UltraFabric is built from written specifications with proof obligations, and parts of it are machine-checked. This page says what of that is public now, what waits on a patent filing, and how a researcher can see more.
10⁷ plans
10,000,000 generated plans checked, 0 wrong answers, 994,405 isolation checks.
Lean 4
Eight rewrite laws and the isolation guarantee for the core operators, proved with no unproved steps.
What is published
Everything in this list is on this site or is given to early-access teams under agreement.
The documentation set
Architecture, storage engine, Ultra IR plan language, security model, SQL and psql, node protocol, how we test, and status. Written from the repository and updated with each phase.
Specifications, under agreement
The system specification and the plan-language specification, each with a proof-obligation register, are shared with early-access teams under agreement. They are not public.
In progressMachine-checked proofs
A dependency-free Lean 4 project in the repository (formal/lean, Lean 4.19, no Mathlib) proves eight optimizer rewrite laws and the tenant-isolation guarantee for the core operators, with no unproved steps, in a CI job. The proofs cover queries without runtime errors; the error rules are tested instead.
BuiltThe ten-million-plan campaign
A nightly runner checks generated plans against a reference interpreter, every optimizer rewrite, the encoding round trip, and an isolation check on every tenth plan. Ten million plans: no wrong answer, no isolation failure. The report and raw file are on the benchmarks page.
What waits
Stated so nobody expects it sooner.
Papers
Papers describing the mechanisms follow a patent filing and are then shared with early-access teams under agreement. No titles or contents are announced before that.
PlannedMechanisms
This site states what the verifier guarantees and how it is tested, not how its rules work internally. That holds for the documentation set as well.
Source
The repository is private during development. The licence model is published with the first release.
What you can check without the mechanisms: the guarantee as stated in the security model, the test method in how we test, and every measurement with its raw file on the benchmarks page.
How a researcher gets more
Two routes, both answered by an engineer on the project.
1Early access
Request a hosted database when early access opens. Early-access teams receive the build, the specifications under agreement, the benchmark and test scripts, and the papers once filed.
Request early access2A written request
Write to [email protected] with your affiliation and what you want to examine: a proof, a specification section, a benchmark re-run. A person on the project answers and says plainly what can be shared now and what cannot.
Start with what is public.
The documentation set and the benchmark reports are written for people who will check.