An RDF/SPARQL engine you can run on your own data — parse it, query it, validate it, transform between syntaxes, canonicalize it, and serve it over HTTP. The engine is specified in F* and extracted to native OCaml, JavaScript, WebAssembly, and C, so the same logic runs on the command line, in Node, and in your browser with nothing on a server.
Read the Shardborough storage specification → for the current Lean 4 block, index, integrity, and update format family. The dated design notes behind it are listed, with their status, in the worknote index.
Explore the documentation Hub → — maintained, runnable RDF/SPARQL notebooks. Start with SPARQL and property paths or the life-sciences named-graph workload. They run in the browser without sending your data to a server.
RDF Core 1.1 in every concrete syntax (N-Triples, Turtle, N-Quads, TriG, RDF/XML), full SPARQL 1.1 (query, update, protocol, service description, entailment regimes), RDFS and OWL 2 RL inference, SHACL and ShEx validation, SKOS integrity, RDFC-1.0 canonicalization, RML mapping, and a read-write on-disk store served over HTTP.
Latest W3C test results are
generated by CI from actual runs and are authoritative. As of
2026-08-14, the runnable W3C 1.1 total is 1661 pass, 0 fail, 1
unsupported (SPARQL 1.1 631 pass, 0 fail out of 631; RDF 1.1 1030
pass, 0 fail, 1 unsupported out of 1031). That total is one lower
than the 1662 reported on 2026-08-12, and the change is an
improvement: rdfs-entailment-test001 used to pass without being
checked at all, and now reports honestly as unsupported, because it
needs rdf:XMLLiteral validity checking this engine does not have
(optional in RDF 1.1). Two other measurement repairs landed the same
day — ten model-theory tests that passed without running any check,
and syntax tests that only asked "did it parse?" rather than "is the
RDF right?" — and both fixes are reflected in this figure.
Performance is measured separately, each number dated and
commit-linked — see the
performance hub.
Three conformance pages state the measured scores per area and name every test that still fails, with its reason and disposition: RDF conformance (the five syntaxes, RDF 1.1 and RDF 1.2 Semantics, RDFC-1.0 canonicalization), SPARQL conformance (query, update, protocol, federation, service description, entailment regimes, and the SPARQL 1.2 Working Draft), and OWL 2 conformance (the nine W3C catalogs under the RL and DL regimes). The RDF and SPARQL pages also separate what is proved — a machine-checked theorem against a formalisation of the specification, stated independently of the code — from what is only measured by a test suite.
The review kernel answers "what do you actually prove" directly: the strongest 1-4 theorem statements per pipeline stage (parser, expressions, filters, modifiers, results, streaming) plus the RDFS entailment/closure chain, each with its exact domain and honest boundary, readable end to end in one sitting — drawn from the full theorem registry of every proved statement.
The per-module assurance inventory
is derived from the F* source and the extracted OCaml, with no
hand-written rows. For every module it says whether the module is
merely total, carries local refinement lemmas, carries an
algorithm-correctness theorem, or carries a refinement theorem against
an independently-stated formalisation — plus its active assume val
count, any admissions, and which official suites exercise it at what
coverage.
Parser and algebra spec are verified in F*; the on-disk backend has unverified OCaml-side optimization layers being migrated back to F*. How Factoidal works covers the verification story, the four extraction targets, the read-write store, and the module dependency graph.