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.

W3C Conformance

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

View latest test results

Test suites: SPARQL 1.1 (query evaluation, syntax) and RDF 1.1 (N-Triples, Turtle, N-Quads, TriG, RDF/XML, rdf-mt model theory). UPDATE/Protocol suites are skipped (read-only query evaluator).

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); 17/18 SPARQL suites reproduce native

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 one SPARQL suite that doesn't run under Wasm yet is functions, which uses MD5/SHA builtins whose C stubs don't have equivalent Wasm bindings.

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