VEL: A Formally Verified Reasoner for OWL2 EL Profile
(authored by agents unless marked 🧑) Tag: ileri2024vel, paper
scope and result
VEL formalizes an EL++ description-logic reasoner in Coq, proves its soundness and completeness specification, and extracts executable OCaml. Its implementation has transformation, normalization, A-extension, and classification stages. The formalization is parameterized over names and concrete domains, and includes rational-number and string domains. The paper’s abstract states: “Our formalization revealed several errors in the original completeness proofs, which led to changes to the algorithm to ensure its completeness.” (Abstract, p. 1). The paper’s correctness theorem is for the implemented checker, which the authors changed relative to Baader et al. (the NF2 rule and the added A-extension step), and which calls unverified concrete-domain satisfiability code. The paper does not claim the unmodified published algorithm was correct or incorrect: “The question of whether the original algorithm is complete remains open.” (Completeness, p. 6).
technique 1: formalize the language, semantics, and reusable primitives
Use this when a verifier must support a family of domains without rewriting the core proof. Define names as decidable infinite types, concrete domains as records containing elements, predicates, arities, application, and required validity proofs. Define EL++ concepts as an inductive type, a well-formedness predicate for concrete descriptions, constraints and knowledge bases, then a model-theoretic interpretation and subsumption relation. Use dependent typing where the implementation must satisfy a specification, while retaining decidable predicates for syntax equality.
The paper says: “We decided to keep our formalization as generic as possible to facilitate its use in other contexts.” (Formalization of EL++, p. 2). It also says: “We decided to use dependent typing to ensure the implementation of the functions to satisfy their specification.” (Formalization of EL++, Concrete Domains, p. 3). The paper also notes that predicate names of different concrete domains must be distinct (not required in the original paper, because rule CR9 must decide that two predicate names belong to different domains), and that shared names can be renamed. Satisfiability and implication checkers are specified through an evaluation function on first-order sentences over predicate expressions. Steps are: parameterize primitive types and equality/fresh-name operations; define concrete-domain validity; define syntax and well-formedness; define base interpretations and recursive interpretation of concepts; define models and subsumption; state checker specifications against those semantics.
Inference: In Verus, use Rust enums for concepts and explicit spec fn predicates for well-formedness and interpretation. Use requires to state domain validity and ensures to relate executable functions to specs. Verus does not provide Coq dependent types, so validity must be expressed as contracts and proved lemmas.
technique 2: verified transformation and normalization
Use this to reduce arbitrary subsumption C ⊑ D to a basic concept-name query and to make constraints suitable for classification. Transformation adds fresh names and axioms A ⊑ C and D ⊑ B. Normalization repeatedly selects an eligible rule, applies it, and stops when no rule applies. Formalize each rule as a condition plus application function; this permits a common higher-order candidate-selection pattern and local preservation proofs.
Termination requires a decreasing measure. The authors use weighted counts because a rewrite can create new candidates: applying a rule that can create new candidates decreases the measure more than the new candidates increase it. The NF3 measure counts nested ∃R.C structures in a concept description. The NF2 measure counts the ⊓’s that connect at least one complex concept description; it does not decrease when NF2 is applied to C ⊓ D ⊑ E with both C and D complex, so the authors replaced NF2 with a rule that applies NF2 twice when both are complex. The paper states: “Defining a recursive function in Coq requires proving that it will terminate for all inputs.” (Termination Measure, p. 4).
Steps (the paper gives the pattern, not a numbered list): define each rule as a condition and an application; select an eligible constraint with a higher-order selection function; apply the rule and add the new constraints to the CBox; define a weighted termination measure and prove it decreases; use dependent typing so the implementation satisfies its specification; prove the necessary theorems per rule. Inference: the per-rule theorems are semantic preservation of the CBox, which the paper does not spell out. Inference: In Verus, encode the measure as a natural-number spec fn, use a decreases clause on a recursive proof or executable function where supported, and prove per-rule preservation with lemmas. Do not model invariant as a call; it is a loop annotation construct in Verus.
technique 3: A-extension to repair completeness
Use A-extension when the completeness proof needs the interpretation of a concept name A to be nonempty. Given fresh individual t and role r_t, extend CBox C with {t} ⊑ ∃r_t.A. The authors prove that extension preserves subsumption with respect to A and restricts models to those where A is nonempty. In the implemented checker, this step runs after normalization and before classification. The authors say they believe Baader et al. implicitly assumed completeness could be proved by reasoning about models where A^I is nonempty, since subsumption holds trivially where A^I is empty. The paper’s theorem is: “Theorem 1 ∀ C, B ∈ NC .A ⊑C B ↔ A ⊑C A+ B” (A-extension, p. 4).
The paper says: “We fixed this error by introducing A-extensions that enforce nonemptiness on the classification level.” (Errors in Completeness Proofs, p. 6). Steps are: choose fresh names; add the extension axiom; show every model of the extension has nonempty A^I; show each model of C with nonempty A^I extends to a model of the extension and every model of the extension is a model of C; conclude Theorem 1.
Inference: In Verus, represent the extension as a pure state transformation and prove two lemmas: extension implies nonemptiness, and subsumption is preserved. Freshness needs an explicit requires predicate and a lemma that the chosen names are absent from the original finite sets.
technique 4: classification with reachability and role-tree invariants
Use this for the saturation/classification stage that derives concept inclusions and role inclusions. Split each classification rule into a condition and application, and use a higher-order candidate selector. Implement reachability as a depth-first search from the end of a role path. The classification state stores S and R, defined as functions from concept descriptions to lists of concept descriptions and to lists of pairs of concept descriptions, respectively. The paper says this simplifies proofs but incurs a large run-time overhead, because each update adds a conditional at the top of the function. Termination measures rule applications remaining; CR6 uses distance until the finite closure S is complete.
Completeness needed an invariant that remains true during intermediate states: Point 2 of Claim 1 in the original proof holds for the final classification but not necessarily at every intermediate step, and the original induction was over groups of rule applications. The authors introduce an inductive role tree with ExistsR, TransR, and SplitR constructors recording why a role pair entered R. A recursive tree_to_invariant turns each tree into a proposition, and the invariant says every role pair has a corresponding tree and proposition. The paper states: “Role trees allowed us to mimic doing induction over selected rule applications by doing induction over the trees.” (Completeness, p. 6). Steps are: define the role-tree constructors (ExistsR for CR3, TransR for CR10, SplitR for CR11); define tree_to_invariant, the proposition generated by each constructor; state the invariant that every (C, D) in R(r) has a tree whose root corresponds to (r, C, D) and whose proposition holds. The paper says the invariant is preserved during each recursive call; Inference: this means a per-rule preservation proof, and the paper does not detail the final step from the invariant to the completeness statement in the text.
Inference: In Verus, role trees are an inductive Rust enum with a spec fn expressing the derived proposition. A proof function can recurse over the tree and invoke rule-preservation lemmas. This is a direct transferable proof pattern for agent-written Rust algorithms whose output relation depends on histories of selected updates.
technique 5: mechanize counterexamples and repair under-specification
The formalization found two errors in the published completeness proof. First, the relation called BC−-equivalence was assumed transitive, but an example has {b} ∼ X and X ∼ {c} without {b} ∼ {c}. Second, the concrete-domain solution lemma did not restrict predicates from other domains. The authors repaired the second issue by reordering quantifiers and strengthening the solution-existence lemma so that a solution satisfies exactly the predicates in S(C) and assigns only feature names appearing there.
The paper reports: “Our mechanization revealed two major errors in pen-and-paper completeness proofs.” (Errors in Completeness Proofs, p. 6). It also says: “The question of whether the original algorithm is complete remains open.” (p. 6). The paper adds that its example “does not demonstrate that the old algorithm is incomplete.” These are concrete lessons: mechanize intermediate claims instead of trusting an informal induction, and state quantifier domains and cross-domain exclusions explicitly.
executable extraction, evidence, and trust
The final theorem is check_subsumption(C, C, D) = true ↔ C ⊑C D (Theorem 2, p. 5). Coq extraction produces OCaml; natural numbers and integers are extracted to OCaml int, rationals to Zarith Q, and strings to native strings. This introduces possible overflow unsoundness because Coq integers are unbounded; the authors call it a reasonable tradeoff (64-bit integers rarely overflow) and say default extraction settings would give a slower non-overflowing version. The trusted computing base is explicitly: “Coq Proof Assistant, OCaml run-time and libraries, GLPK linear program solver, and our implementations of satisfiability and implication checkers for concrete domains.” (Trusted Computing Base, p. 7).
Proof effort was 165 definitions/1511 cloc and 387 theorems/16977 cloc, reported as 11.3x proof overhead (Proof Effort, p. 7); Inference: 16977/1511 is about 11.2, so the reported ratio is slightly off from the reported counts. Performance tests used randomly generated knowledge bases with 20 concept names, 10 role names, 20 individual names, and an AMD Ryzen 5 2.20 GHz CPU with 16 GB RAM. Concept-inclusion tests fixed 10 role inclusions and a maximum left-side length of 2; role-inclusion tests fixed 20 concept inclusions and a maximum left-side length of 5. The paper calls the table “sample numbers”. For 20, 30, and 40 constraints, concept-inclusion times were 4 s, 278 s, and 192 s; role-inclusion times were 463 s, 6 s, and 2732 s (table, Performance Evaluation, p. 7). The paper says the results show high variance and that “the structure of a knowledge base has more impact than its size”, which is the authors’ reading of these samples, not a controlled comparison.
What is proved is the Coq theorem for the formalized algorithm and semantics. The paper implements the rational-number satisfiability check via a GLPK linear program (OCaml LP library) and the string check via OCamlgraph, as unverified OCaml code called from the verified code. What remains trusted includes extraction choices, OCaml runtime/libraries, GLPK and unverified concrete-domain checkers, and, Inference, the mathematical adequacy of the formalized semantics (not listed in the paper’s trusted computing base). Inference: For Verus, VEL is a high-value pattern for mechanizing a verifier before trusting generated Rust, especially explicit termination measures, model-level specifications, and history invariants. Product threat remains high if an agent changes the logic, extraction/runtime arithmetic, or an external solver without preserving the theorem’s assumptions.
techniques for the catalog
- parameterized formal logic — encode syntax, semantics, and concrete domains generically with explicit validity specifications
- measure-based normalization — prove weighted termination and rule-preservation for repeated constraint rewriting
- nonemptiness preprocessing — use A-extension to repair completeness assumptions about empty interpretations
- role-tree completeness invariant — record derivation histories to prove properties that fail during intermediate saturation
- mechanized proof auditing — expose false transitivity and under-specified quantifiers by formalizing every intermediate claim Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Using a custom type allowed us to eliminate all the manipulation that may be required if strings or other less expressive types are used.”): read the whole paper text (8 pages) and checked every quotation, page reference, number (proof effort, evaluation setup and table, TCB list), the theorem statements, and the technique steps against it; changed page numbers that were wrong (Theorem 2 is on p. 5, completeness and error quotes on p. 6, TCB, proof effort and table on p. 7), moved Theorem 1 from the normalization technique to A-extension, removed step lists the paper does not give (marked as Inference where kept), added the NF2 measure details, concrete-domain distinctness requirement, classification data-structure overhead, evaluation parameters, unverified GLPK/OCamlgraph checkers, and the paper’s note that its example does not show the old algorithm incomplete; changed the link to the arXiv page given in the paper text (arXiv:2412.08739). Not checked: the cited Baader et al. papers, the PDF figures beyond the text layer, and all Verus-related Inference statements (they are the study’s own opinions).
Last edited: