Factoidal

A formally verified RDF/SPARQL implementation. The F* specifications are the product. Executable code is obtained by extraction, not hand-written.

Try it in your browser

Launch the SPARQL demo →

Paste Turtle data, write a query, see the results — the engine is F*-extracted OCaml compiled to JavaScript; nothing runs on a server.

Module dependency graph

The F* spec is split across 90 modules. The interactive dependency graph shows what depends on what — derived from fstar.exe --dep graph so the edges match what the build sees. Static SVG / PNG / Graphviz / Mermaid / plain-text renders are shipped alongside.

W3C Conformance

Current pass/fail numbers are generated by CI from actual test runs.

View latest test results

Test suites: SPARQL 1.1 (query, update, protocol, service description, entailment regimes), RDF 1.1 (N-Triples, Turtle, N-Quads, TriG, RDF/XML, rdf-mt model theory), RDFC-1.0 dataset canonicalization, and the OWL 2 RL profile catalogs. As of 2026-07-03 the runnable W3C total is 1662 pass, 0 fail (SPARQL 631, RDF 1031) — the dashboard is regenerated by CI on every push and is authoritative.

Performance (measured, dated, commit-linked)

Speed is measured separately from correctness — each number below names its date and the commit it was measured on.

What Measured Date / commit
Turtle parsing ~100k triples/s, near-linear to 1M triples (1M in 9.66s) 2026-07-03, 11ba254
In-memory dataset, end-to-end (parse + index + GRAPH-count query) 1M quads in ~41s, ~1.2 GB peak RSS (~1.2 KB/quad) 2026-07-03, 723db3c
OWL-RL closure, sameAs 32-clique (was >590s cap-trip) 1.07s — closure step reduced from O(k⁶) to ~O(k³) 2026-07-03, 4812c3d
On-disk COTTAS (WIP) serves the 3,143,406-quad UK Parliament corpus (live demo); fast paths still unverified OCaml being migrated to F* issue #118

Build targets

The same F* source is extracted once and then compiled for three runtimes:

Target Output Status
Native bin/<platform>/w3c_runner, bin/<platform>/factoidal full W3C pass counts
JavaScript (js_of_ocaml) /fstar-extracted/w3c-runner.js runs in any modern browser or Node
WebAssembly (wasm_of_ocaml) /fstar-extracted/w3c-runner.wasm.js + .wasm.assets/ Wasm-GC engines (Chrome ≥ 119, Node ≥ 22); experimental — cross-runtime parity tracked in tests/beyond-w3c/ (hash builtins are pure OCaml now, removing the old MD5/SHA C-stub gap)

The artifacts are rebuilt by CI on every push and ship from docs/fstar-extracted/. The Wasm binary links a vendored copy of zarith_stubs_js's runtime.wat + runtime_wasm.js to wire the ml_z_* arbitrary-precision integer primitives through to JavaScript BigInt. The hash builtins (MD5/SHA family) are realised in pure OCaml (fstar_pure_hashes.ml) specifically so native, JS, and Wasm builds share one code path — the historical functions-suite Wasm gap came from C hash stubs and no longer applies.

Architecture

F* formal spec  (the product)
    |
    v
fstar.exe --codegen OCaml
    |
    ├── ocamlfind ocamlc     → bin/<platform>/w3c_runner      (native)
    ├── js_of_ocaml          → docs/fstar-extracted/w3c-runner.js
    └── wasm_of_ocaml        → docs/fstar-extracted/w3c-runner.wasm.{js,assets/}

See formal/fstar/build-ocaml.sh for the exact invocation.

Source