Platform · How It Works in depth

The Compiler, in Depth

The payoff for your team: the software you build on is generated from the proof itself — never hand-transcribed from it, so it cannot drift from what was verified, in whichever of the six supported languages you work in.

This page goes under the hood of how a proved theory becomes software. There are two compilers, never one, and they do different jobs: OntoEnact turns proved CLIF into the SDKs your teams build on, and OGSL turns the same proved theory into the schema the runtime graph engine executes. Both sit behind the same prover gate. It is written for developers and technical evaluators, with a short summary above each diagram so the through-line stays clear whether or not you read the diagrams themselves.

Back to How It Works
Two compilers

One Proved Theory, Two Compilers

A verified theory is compiled twice, for two different purposes. Naming them apart matters, because they take different inputs, produce different outputs, and target different languages.

ontoenactc
The OntoEnact Compiler

Compiles BFO CLIF into the software your teams build on.

In  CLIF modules, ISO/IEC 24707, grounded in BFO 2020
Out  native SDKs, Knowledge Explorer consoles, proof certificates, PROV-O provenance, NativeAOT bindings
Targets  C#, Rust, Go, C++, Java, Python — six
ogslc
The OGSL Compiler

Compiles the graph schema the runtime engine executes against.

In  .ogsl schemas and .cl theories
Out  storage schema, wire protocols, graph algorithms, zero-copy cell accessors
Targets  C#, Rust, Go, C++, Java — five, statically typed only

The bridge between them. A CLIF-to-OGSL emitter projects the verified theory into an OGSL schema, so the graph structure is derived from the same proved axioms the SDKs came from instead of modelled a second time by hand.

That is why the target counts differ, and the difference is deliberate. Six is the SDK surface, where a developer consumes entity types and queries. Five is the graph surface, held to statically typed targets with zero-copy memory access. A dynamically typed target would receive the names and lose the guarantees.

The OntoEnact compiler

ontoenactc — Proved Theory to Native SDKs

This is the compiler behind the deliverable. It loads the module graph, puts the assembled theory through the prover gate, and only then emits. Nothing downstream of the gate runs if the gate does not pass.

What one run does
  1. Validate and load. The ontology registry is read and the module graph resolved, transitive dependencies included.
  2. Verify. The assembled theory goes to the prover portfolio. This is the gate: a failure stops the run rather than warning and continuing.
  3. Emit canonical CLIF. The authored theory is written back in normative form, so what was proved and what is published are the same text.
  4. Generate SDKs. Six languages from one verified source, carrying entity types, registries, query providers and validation logic.
  5. Generate consoles. A Knowledge Explorer ships beside every SDK.
  6. Bind and package. NativeAOT C-ABI bindings, then per-language packages and publication to the SDK store.
The OGSL compiler

ogslc — Proved Theory to Graph Schema

Only after a theory is proved does the compiler run. It extracts the verified axioms, resolves the BFO module system, and lowers everything to a common intermediate form before any target-language code is emitted, so the software your teams build on is generated from the proof itself, never hand-transcribed from it.

The ogslc compiler pipeline from OGSL inputs through parsing and validation to generated output, failing loudly when a schema resolves to zero axioms.
The ogslc pipeline. A schema that resolves to no axioms stops the build instead of emitting an unverified graph.
OGSL polyglot code generation: one BFO-grounded schema and one intermediate representation emitting five statically typed languages, with Python served by the OntoEnact compiler instead.
One schema, one IR, five languages. Python is deliberately absent here. It is served by ontoenactc, for the reason set out above.
It also writes the graph algorithms, in every language

Because the compiler knows which fields are edges and which are nodes, it can generate the traversal work instead of leave it to you. Thirteen algorithms are emitted for each of the five targets, against the same zero-copy accessors as the rest of the schema:

Breadth-first and depth-first search · shortest path · weighted shortest path · topological sort · strongly connected components · connected components · PageRank · community detection · minimum spanning tree · maximum flow · minimum cut · cycle detection

The point is not the list, which any graph library can match. It is that these are generated against your schema, so they operate on your own entity types rather than on an untyped node-and-edge abstraction you have to map back to your domain afterwards.

The OGSL Compiler — ogslc

Four stages, run in order, with the theorem prover standing between the knowledge and the code. No proof, no emit.

Inputs .ogsl schemas .cl CLIF theories Two front ends, one common internal form, either route arrives at the same verified core.
1 Parse

Reads your schemas and theories and turns them into one internal form, checking as it goes that what you wrote means what you intended.

→ Ontological IR
How it works

A reactive lexer feeds a parser-combinator grammar to produce an AST, followed by semantic analysis across BFO, CLIF, mereology, and graph layers. Symbol resolution runs in two passes so definitions can reference each other across files. Everything lowers to a single BFO-grounded Ontological IR, both front-ends converge there.

2 Verify, the gate

The theorem provers run here, and nothing proceeds without them. This is the step that makes the rest of the pipeline trustworthy and not merely fast.

fails loudly instead of passing silently
How it works

Axioms are extracted and checked against a cache of thirteen BFO 2020 top-level ontology theories, then dispatched to the prover backend — z3, cvc5, vampire, and ontoprover, for consistency, proof, entailment, and counter-model checks. If a schema yields zero axioms the compiler fails loudly instead of emitting something vacuously valid.

3 Emit

Generates the graph-engine source in five statically typed languages from the verified form, the same meaning in each, not five hand-written interpretations of it.

byte-identical output
How it works

The IR feeds the polyglot generators, which emit C#, C++, Go, Rust and Java source, plus graph algorithms and optional NativeAOT FFI bindings. Given the same input the output is byte-identical, so a build can be reproduced and diffed rather than trusted.

4 Pack

Wraps the generated code as libraries your developers install the ordinary way, through the package manager they already use.

→ redistributable packages
How it works

Per-language manifests are written for NuGet, Cargo, Maven, go.mod, and CMake, alongside CI configuration, documentation, and provenance records. A build flag hands the whole thing to the BuildExecutor, so packaging is part of the compile and not a separate manual step.

Proof before code, no proof, no emit

A schema is proved consistent before a single line is generated. The theorem prover is the gate, not a linter, and not a check run after the fact when the code already exists.

How it works

The compiler reaches the prover through a client interface that supports in-process, gRPC, and automatic hybrid connectivity, so the same gate holds whether verification runs on a developer’s machine or against a shared service.

The loop closes, verified logic back to editable schema

Verified CLIF converts back into a canonical, human-editable schema that re-enters the pipeline, so knowledge can be refined by the people who own it without leaving the verified path. Every conversion is graded for how faithfully meaning survived:

Translatable Transitively translatable Degraded Rejected
How it works

Emitted schemas carry SHA-256 provenance and a trust grade, so a downstream reader can tell whether a definition translated cleanly, translated through intermediate steps, lost fidelity, or was refused outright, instead of discovering the loss later.

If the theory does not prove, there is nothing to ship.

Powered by OntoMotion™

OGSL Compiler — Polyglot Code Generation

One schema, one verified internal form, five independent emitters, so a fix made once reaches every language rather than being reimplemented four more times.

The pipeline
One .ogsl schema
→
Proved consistent
→
One internal form
→
Five emitters
→
Byte-identical SDKs

The five targets are not equally mature, and we would rather say so than make a flat claim. Each tier below is earned by that language’s own compiler building the output, never by our inspection of it.

C#
Production
C# 14 · .NET 10

The reference target, the engine itself is built from it, so this is the most exercised path. Production means we build our own engine on this output.

How it works

Emits SDK types with zero-copy accessors, LINQ and LIKQ selectors, and gRPC graph-engine client bindings.

Rust
Toolchain-verified
edition 2021

Builds cleanly under Rust’s own toolchain, with one area still being finished. Toolchain-verified means that language’s own compiler builds the generated code cleanly, for single-namespace schemas.

How it works

cargo build completes clean for single-namespace schemas, emitting a crate with resolved dependencies. Multi-namespace support has one module still pending.

Java
Toolchain-verified
Java 21

Compiles under Maven, using modern language features and not legacy scaffolding. Toolchain-verified means that language’s own compiler builds the generated code cleanly, for single-namespace schemas.

How it works

mvn compile completes clean for single-namespace schemas, emitting records and sealed classes in a standard Maven layout.

C++
Toolchain-verified
C++23

The data-model core compiles today; full multi-header builds are still in progress. Toolchain-verified means that language’s own compiler builds the generated code cleanly, for single-namespace schemas.

How it works

The core compiles under g++ -std=c++23 with zero-copy accessors. Assembling the full multi-header translation unit is pending.

Go
Emitting
Go 1.22

The least mature target, the data surface emits, but it is early. Emitting means code is generated and is structurally correct, but we do not yet claim a clean build across the range.

How it works

Structs and the data surface emit today. Multi-namespace handling is open, and module-name handling in go.mod is still being refined.

The query language is ported, not wrapped

Most polyglot SDKs give one language a real API and the rest a thin wrapper over it. The graph query surface here is compiled into each language’s own lazy-iteration machinery instead, so a developer writes queries the way their language already does them. Same query, same semantics, five native idioms.

Language Query surface Built on
C#LINQ and cell selectorsIEnumerable, async
C++std::rangesC++23 ranges, std::generator, co_yield
RustIterator traitIterator adaptors, lazy evaluation
JavaStream APIjava.util.stream, parallel streams
Goiter.SeqGo 1.23 range-over-func, generators

The mapping goes operation by operation. A filter becomes .Where() in C#, std::views::filter in C++, .filter() in Java, and .where_() in Rust. A limit becomes std::views::take, .limit() or .take(n). Nothing is materialised early to make the port easier, so laziness survives the crossing.

Verified by compilation, not by inspection

A target is promoted only when its own toolchain compiles what we generated. That is why the tiers above are honest, and why one fix to the shared internal form improves all five at once instead of five separate repairs.

How it works

All five emitters lower from one shared intermediate form and are covered by roughly 1,900 code-generation test cases across seven test projects, including FsCheck property-based tests and golden-output checks in each language. Output is byte-identical run to run — build timestamps were removed so determinism is real and a build can be diffed instead of trusted. Cross-language interop uses ahead-of-time-compiled bindings passing plain data structures rather than serialized JSON. Python and TypeScript are deliberately excluded from this compiler: the graph schema layer stays on statically typed targets that support zero-copy access. Python remains a first-class target of the OntoEnact SDK compiler described above.

Five targets at five levels of maturity, and we publish which is which.

Powered by OntoMotion™
Founding Partner Program

Want to walk your engineers through the compiler? Let’s set up a technical session.

Request a Demo