RDF conformance — measured scores and every named residual#

Factoidal runs the W3C RDF test suites from disk, through the F*-extracted parsers, canonicaliser and entailment engines, and reports the result per suite. This page states the scores as measured, defines the entailment regimes they are measured under, names every test that still fails or is skipped with the reason and its disposition, and separates what is proved from what is only measured.

Every number below comes from one re-run of every RDF suite against the committed bin/linux-x86_64/w3c_runner and bin/linux-x86_64/rdfc10_runner binaries on 2026-07-30, from the repo root, at tree 873aed4. Nothing here is copied from a document. The machine-readable copy is the test-results dashboard and its latest.json; a number here that disagrees with that file is a bug in one of them, not a judgement call.

Parser and algebra spec are verified in F*; the on-disk backend has unverified OCaml-side optimization layers being migrated back to F*.

Sibling pages: OWL 2 conformance · SPARQL conformance · per-module assurance inventory.

What each entailment regime means#

The RDF suites are not all syntax. Three of them (rdf-mt, rdf12entail, and the entailment part of the OWL/SPARQL work) score an entailment question: does graph A entail graph B? The answer depends entirely on which regime you ask under, so the regimes are stated first and the dispatch is stated with them.

Simple entailment. No vocabulary has any special meaning. A entails B exactly when there is a mapping of B's blank nodes to terms of A that turns every triple of B into a triple of A — a graph homomorphism. IRIs and literals are compared as syntax; nothing is derived. This is the weakest regime and the only one for which this project has a machine-checked soundness and completeness proof (see what is proved below).

RDF entailment. Simple entailment plus the RDF axiomatic triples and the rule that every predicate is an rdf:Property (rdfD2), plus recognised-datatype value equality — so "1"^^xsd:integer and "1.0"^^xsd:decimal denote the same thing, and an ill-typed literal in a recognised datatype makes the graph inconsistent.

RDFS entailment. RDF entailment plus the RDFS rules: rdfs:domain and rdfs:range type their subjects and objects, rdfs:subClassOf and rdfs:subPropertyOf propagate and are transitive, container membership properties are sub-properties of rdfs:member.

D entailment (datatype entailment). Parameterised by a set of recognised datatypes: literals are compared by value in those datatypes rather than by lexical form, and a literal whose lexical form is not in its datatype's lexical space makes the graph inconsistent. RDF and RDFS entailment are both defined on top of a D-entailment step.

Which regime each runner actually dispatches#

So the two entailment suites are checked by two different engines, and only one of them is the F*-extracted one. That is stated here because it changes what a green rdf-mt row means; see what is proved.

Scores#

The one unsupported RDF 1.1 test is rdfs-entailment-test001 in rdf-mt. It requires checking whether an rdf:XMLLiteral value is well-formed XML, which this engine does not do; RDF 1.1 makes XMLLiteral support optional. Until 2026-08-14 this test reported PASS without being checked at all — the runner returned Pass before any entailment function ran. It is now reported honestly, which is why the RDF 1.1 total reads 1030 rather than 1031.

The RDF 1.2 rows break down per leaf manifest as: N-Triples syntax 29, N-Quads syntax 27, Turtle syntax 67, Turtle eval 29, TriG syntax 35, TriG eval 25, RDF/XML eval 30 — each 0 fail, 0 skip; and c14n N-Triples 41, c14n N-Quads 41, each 0 fail, 0 skip.

RDF 1.2 and its suites are W3C Working Drafts, not Recommendations. A green row there is progress against a moving target.

The denominators, checked independently#

Every denominator above was re-derived from the mf:entries list of each manifest, not taken from the runner. They agree exactly: 70, 313, 87, 356, 166, 39 (sum 1031) for RDF 1.1; 242 and 82 and 47 for the RDF 1.2 suites; 86 mf:action entries for rdfc10.

Twelve further test descriptions exist in those manifests but are commented out of the mf:entries list upstream, so they are outside every denominator on this page. They are not skips — a skip is work we intend to do; these are tests the W3C suite itself withdrew:

A manifest defect in this repo's own suite wiring#

Six .github/test-suites/*.yaml manifests — rdf-turtle, rdf-xml, rdf-trig, rdf-n-triples, rdf-n-quads and rdf-mt — declare log_path: formal/fstar/ocaml-output/sparql_results.log. That file carries the SPARQL score lines. The RDF suites' scores are in rdf_results.log. Anything that resolves an RDF suite's score by reading its declared log_path and taking the file total will read 631 (the SPARQL 1.1 total) where the correct answer is the per-suite label, e.g. 313 for rdf-turtle. That mis-resolution has already happened once in draft prose for this page. Resolve by exact suite label, never by file total, until the manifests are corrected.

Disposition vocabulary#

Each residual carries one of five labels, from the completeness ledger's fixed vocabulary (issue #308):

• by-design — the test asks for something outside what this engine claims, citing the suite's own metadata or a written scope decision.
• planned-family — a real gap in a named family of missing behaviour, tracked and intended.
• dependency-blocked — waiting on a capability elsewhere in the engine.
• disputed-fixture — the fixture itself is defective or its expected verdict does not follow; documented per test.
• environment — toolchain or harness, not semantics.

Residual failures — RDF 1.2 Semantics (3 of 47)#

These are the only failing tests in any RDF suite measured on this page. All three are mf:PositiveEntailmentTests reported as "Should entail but doesn't" — under-derivation, never a wrong entailment. Every fixture below was read, not inferred from the test name. All three carry rdft:approval rdft:NotClassified: the RDF 1.2 Working Group has not approved them.

Skipped tests — RDF 1.2 Semantics (3 of 47)#

Skips are reported by the runner, counted in the denominator, and named here rather than dropped.

Harness note the literal-type skip exposes#

The Turtle parser used to load manifests (parse_turtle_fstar) drops a statement that uses an undeclared prefix and carries on, instead of rejecting the document. Measured directly: a three-statement file whose middle statement uses an undeclared prefix parses to the other two statements and exits 0. The document-level guard only fires when the result is empty ("parsed to zero triples but is not an empty document", issue #325), which is why the five turtle-syntax-bad-prefix-* negative tests still pass — they are single-statement files, and they are additionally scored through the separate strict path parse_turtle_strict, which does reject. The W3C Turtle suite contains no multi-statement undeclared-prefix fixture, so this leniency is invisible to the score and visible only here.

Passes that are decided without running an entailment check#

rdf-mt reads 39 pass, 0 fail (out of 39). Ten of those 39 are decided by the harness before any entailment or consistency question is asked. This is measured, not inferred: replacing a fixture with non-RDF text and re-running the suite shows which verdicts change.

• Seven mf:PositiveEntailmentTests carry mf:result false — they assert the premise is inconsistent. The runner has no inconsistency check, and its positive-entailment arm returns Pass as soon as it sees "action file present, no result file". Verified by replacing rdf-mt/datatypes/test006.nt with the line this is not RDF at all @@@ <<< >>>: datatypes-range-clash still reports PASS. Deleting the file instead turns it into Skip "Action file missing", so the pass is conditioned on file existence and nothing else. The seven are datatypes-non-well-formed-literal-2, datatypes-range-clash, datatypes-test010, rdfs-entailment-test001, rdfs-entailment-test002, xmlsch-02-whitespace-facet-2, xmlsch-02-whitespace-facet-4.
• Three mf:NegativeEntailmentTests carry mf:result false — they assert the premise is not inconsistent. The runner's arm for these loads the premise and passes if loading raised nothing; the runner's own comment says "For now, just check action parses." Verified by replacing rdf-mt/rdfs-subClassOf-a-Property/test001.nt with non-RDF text: rdfs-subClassOf-a-Property-test001 still reports PASS. The three are datatypes-intensional-xsd-integer-decimal-compatible, datatypes-non-well-formed-literal-1, rdfs-subClassOf-a-Property-test001.
• The other 29 do bite. Verified by replacing the expected graph of datatypes-semantic-equivalence-within-type-1 with an unrelated triple: the test flips to FAIL: Entailment failed: action has 11 triples (after closure), expected 1.

So the defensible reading of the row is: 39 pass, 0 fail (out of 39), of which 29 are decided by an entailment check and 10 by the presence or loadability of a file. The ten are the RDF 1.1 Semantics inconsistency tests, and inconsistency detection is the same planned-family gap that skips malformed-literal in RDF 1.2. Both are tracked under #305 P9; the RDF 1.1 side additionally deserves the honest-verdict treatment OWL got in #326, where an answer the engine did not compute scores unsupported rather than pass.

Disposition counts#

Across the 6 distinct tests that fail or are skipped in any RDF suite — all six in rdf12entail; every other RDF suite is at 0 fail, 0 skip:

The ten rdf-mt file-existence passes are counted separately and carry no disposition label from this vocabulary, for the same reason OWL's unsupported verdicts do: they are not answers the engine got wrong, they are questions it did not ask.

What is proved versus what is measured#

The rest of this page is measurement. This section is the part that is not. For the strongest proved statements read end to end in one sitting — parser, N-Triples/N-Quads round-trip, streaming, and the RDFS entailment/closure chain, each with its exact domain and honest boundary — see the review kernel; the full theorem registry carries every proved statement (~140 rows).

Three claims are easy to blur together, and the project keeps them apart deliberately (issue #313): a module can be implemented in F*, accepted by the F* verifier, or proved correct against a formalisation of the spec stated independently of the code. The third is rare. The machine-derived, hand-edit-free record of which module is which is the per-module assurance inventory — its oracle is extraction, and it fails downward, so a module is under-credited there rather than over-credited.

⚠️ One caveat on the inventory's numbers, from #328: its theorem-class counts depend on build state, because the oracle asks whether a module's extracted .ml exists on disk and 12 of those files are gitignored. In fresh-clone / CI state the tool reports 30 W3C-refinement theorems; after a local ./build-ocaml.sh extract it reports 0. Every figure quoted below was re-derived on 2026-07-30 in a fresh worktree with no local extract — the same regime that produced the committed artifacts — and matched them exactly. The assume val, admission and --lax counts are pure source scans and never flip; the shipping-function counts quoted here are stable too, because every module named on this page has its extracted .ml tracked in git.

Proved: simple entailment, soundness and completeness. RDF.Entailment.Simple.simple_entails — the shipping blank-node homomorphism search — carries 17 refinement theorems against declarative relations defined in separate, fully-erased specification modules (RDF.Entailment.Simple.Spec, .Refinement, .ModelTheory, .Boundary). They include simple_entails_complete, simple_entails_sound, simple_entails_iff_spec, the model-theoretic simple_entails_iff_model_theory, blank-node-label independence (simple_entails_rename_invariant), the same refinement at the parameterised engine entails_with that the RDF 1.2 regimes call, and a parser-boundary theorem entails_ntriples_boundary on Parser.NTriples.parse_ntriples_strict. No admits, no --lax, z3 4.13.3. Design note: docs/designissues/2026-07-29-simple-entailment-refinement.md.

The soundness theorem is conditional, and the condition is stated as a theorem too. simple_entails_sound requires graph_exact on both graphs; simple_entails_not_sound_unconditionally is a machine-checked counter-example showing that without it the shipping function accepts an entailment the specification denies — two literals whose language tags differ only in case. That is tracked as #324. A conditional soundness proof plus a machine-checked witness for the missing case is a stronger honesty position than an unconditional claim, and it is the reason this vertical is worth pointing at.

Landed 2026-07-30 — the RDF and RDFS rungs#

The two refinement agents that were in flight when the table below was measured have both landed. The table describes the shipping modules, and it is still accurate: no shipping module changed. The declarative relations live in separate, fully-erased companion modules.

Neither Spec module opens RDFS.Closure, OWL.Closure, RDF.Graph.Executable or RDF.Entailment.Regime, so each can be diffed against the W3C text on its own. All four verify with no admit and no --lax, under z3 4.13.3.

Seven of the shipping rules now carry a transcription-fidelity theorem (rdfD2, rdfs2, rdfs3, rdfs5, rdfs7, rdfs9, rdfs11, plus container membership): every triple the rule emits is in the seed graph or is derived from the source graph by one application of the rule row it claims to implement. The model-theory module then proves every row of the rule tables truth-preserving, and lifts that through one closure step to the fixed-point driver.

⚠️ The fixed-point theorem has no machine-checked instance (#338). Its hypothesis closure_chain_wf cannot be discharged for a single graph, including the empty one, because sp_key is not proved injective — and it is not injective on IRI subjects alone, since is_iri admits a control character. The hypothesis is true of any graph avoiding U+001F, so the theorem is not vacuous; what is missing is anyone able to instantiate it. The per-rule truth-preservation theorems above are unaffected. A theorem nobody can instantiate carries no assurance until someone can, so this row should be read as pending, not as closure soundness established.

The condition bundle those theorems quantify over is now proved consistent, and proved to admit a model that falsifies a graph — so rdfs_entails is a proper relation and the soundness theorems are not vacuous for that reason either. Both were unproved before 2026-07-30; see docs/designissues/2026-07-30-hypothesis-satisfiability.md.

🔴 The attempt found four gaps, tracked as #335. RS-1 is an unsoundness in shipping code: rdfs_reflexivity_axioms harvests reflexive rdfs:subClassOf / rdfs:subPropertyOf triples more widely than any RDFS rule licenses, and the witness reflexivity_axioms_not_rdfs_sound is hypothesis-free. RS-2 is six rule rows with no implementation — rdfs1, rdfs4a, rdfs4b, rdfs8, rdfs13 and rdfD1 — plus unseeded axiomatic triples. RS-3 is rdfs_rule_range dropping literal objects, which the specification forces: the rule's conclusion moves the object into subject position, and RDF.Term.subject is IRI-or-bnode only. RS-4 is the rdf12 manifests' "RDFS" regime running none of rdfs1–rdfs13, because two functions share the name rdfs_closure.

Design note: docs/designissues/2026-07-30-rdf-rdfs-entailment-refinement.md.

The SPARQL vertical landed the same day; see the SPARQL conformance page.

Measured, not proved: everything else on this page.

Across the whole tree the inventory reports 6 modules with a W3C-refinement theorem, 7 with an internal-refinement theorem, 19 with an algorithm-correctness theorem, and 139 modules that are merely Tot — out of 194 analysed. Zero active admissions, zero --lax/--admit_smt_queries regions, 143 active assume val declarations (iron rule #3 classifies each as an acknowledged gap with an issue or an allowed realisation).

The short version, in the review's own framing: RDF simple entailment is proved. The syntax parsers, the canonicaliser, the RDFS closure beyond rdfs2, and the rdf-mt harness are implemented in F* (except the last) and measured against the official suites. Those are different claims and this page will not merge them.

Where the numbers live#

• Live scores and history: test-results dashboard.
• Per-module assurance: assurance inventory.
• Per-suite disposition ledger: docs/claude-rules/w3c-completeness-ledger.md.
• Tracking issues: #305 (RDF 1.2 / SPARQL 1.2 epic, phase P9 is RDF 1.2 semantics), #313 (claim discipline), #324 (the conditional-soundness witness), #325 (parser soundness on non-ASCII input and the empty-parse guard).
• How the pieces work, with runnable cells: triples and Turtle from first principles, canonical graphs (RDFC-1.0), RDF 1.2 triple terms.