Open Ontologies
A single Rust binary that plans, applies and rolls back changes to a production ontology, reports every consequence of a change before it is applied, and produces a Lean 4 proof of the result that a reviewer can re-check without trusting the tool.
Given a change, Open Ontologies derives its consequences, a "blast radius," and has a Lean 4 checker prove the derived edges; the checker rejects a forged or unsupported line, returns a nonzero exit code, and names the rule that failed, so a reviewer can verify the proof independently rather than trust the tool's output. An example run shows one added triple with zero blast radius producing 901 new consequences that were not present before.
The project also uses its engine to check existing published ontologies for internal consistency; comparing an RDFS file and an OWL file that both claim to describe the same domain, it reports terms used as a class but never declared, ambiguous range declarations, near-duplicate names, and named classes a tableau reasoner or HermiT judges unsatisfiable.
A spreadsheet can be turned into an ontology with evidence for each line through a hosted version of the same engine. The engine itself is MIT licensed; a hosted platform adds enterprise support.