Platform · How It Works

How Your Knowledge Becomes Software

TruSpark™ takes what your organization knows, checks it for contradictions and gaps before any code exists, and turns it directly into working software, then keeps the two aligned as your knowledge changes.

On this page
The Reasonics Methodology

OntoMotion™ — Knowledge and Software, Kept in Motion

Everything TruSpark does runs on a single governing approach Reasonics calls OntoMotion™, the method that turns what your organization knows into working software and keeps the two aligned for as long as you operate it. It is the core of how we work, and it is what makes the rest of this page possible.

In conventional software, the code and the model of what it is supposed to do (a schema, a specification, a diagram) live side by side and slowly drift apart. The documentation stops matching reality, and what the organization knows stops matching what the software does.

OntoMotion inverts that. Your knowledge, the formal definition of what your organization knows, is the single source of truth, and the software is generated from it and not maintained beside it. Nothing the platform produces can contradict the knowledge it was built on.

And it is continuous, never a one-time build. OntoMotion runs the same five-step loop every time your knowledge changes — read each step in plain terms, or open it for the engineering detail.

The loop, in five moves ↻ repeats on every change
Formalize → Prove → Generate → Enact → Govern
01
Formalize
Capture what your organization knows as an explicit, formal definition of how your domain works.
Engineering detail
The engineering view

Your domain is authored as a BFO 2020–grounded ontology in Common Logic (CLIF), or lifted from existing OWL, OBO, or SKOS sources through verified translators, no hand-written logic required.

02
Prove
Confirm the definition holds together before anything is built from it, a contradiction is caught here, at the source, not in production.
Engineering detail
The engineering view

A portfolio of automated theorem provers — OntoProver™ with Z3, CVC5, and Vampire — checks the theory for consistency and returns honest three-valued verdicts. No proof, no code: nothing is generated from an unproven theory.

03
Generate
Turn the proven definition directly into working software, the software is the knowledge, never a document about it.
Engineering detail
The engineering view

The verified theory compiles to build-ready SDKs in six languages, each carrying a replayable proof certificate (TSTP, Alethe, SMT-LIB). C# is production-grade today; Rust, Go, Java, C++ and Python are advancing.

04
Enact
Put that software to work at the decision points that matter, over your real data.
Engineering detail
The engineering view

Generated types run over live instance data through the OntoTelliect™ graph engine, with workflows proved sound before they execute (Sequent) and every decision auditable as it happens.

05
Govern
Keep meaning and software aligned over time — when your knowledge changes, everything downstream re-proves, regenerates, and re-deploys.
Engineering detail
The engineering view

Because the software is generated from the theory instead of maintained beside it, a knowledge change re-runs the whole loop under proof, with licensing, entitlement, and a replayable audit trail governing what ships (Tessera™).

Inputs & Outputs

What Goes In, and What You Get Out

You do not have to start from scratch, and you do not have to speak the language of formal logic to put knowledge in. Getting there is a collaboration: in the early stages, Reasonics works alongside your experts to capture and formalize what your organization knows, a guided knowledge-transfer step, not an automatic one.

Existing ontologies in OWL, OBO and SKOS lifted into the platform with their annotations and provenance intact, with the lift itself running as a verified workflow.
Your existing work comes with you. Ontologies you already maintain are lifted in with their annotations and history intact, and the lift itself runs as a workflow the platform verifies first.

What can go in, and what comes out.

Goes in ⟶

OWL ontologies
OBO Foundry ontologies
SKOS vocabularies
Direct CLIF authoring
Visual authoring (OntoLogic Portal™)
TruSpark

⟶ Comes out

Native SDKs in six languages
Knowledge Explorer consoles
Proof certificates
Provenance records
Graph schemas
Where your work fits

TruSpark generates the verified core, the part that carries your organization's meaning and does the reasoning. Your teams build the application around it — the interfaces, the integrations, the experience, exactly as they do today. TruSpark does not replace your developers. It gives them a core they can trust and never have to hand-maintain.

Already have an ontology in OWL, OBO, or SKOS?

You point TruSpark at the source and the platform does the rest. Each format is lifted into TruSpark's formal representation automatically, with its annotations, provenance, and BFO alignment preserved intact, and no manual conversion step. From there it enters the same pipeline as knowledge authored natively, one of the input channels shown above.

Can you author new formal knowledge without hand-writing logic?

Yes. New formal knowledge is authored through typed programming constructs in C#, where the formal knowledge file is a generated output instead of hand-written input, and every axiom carries an explainability provenance label. Visual authoring through the OntoLogic Portal IDE, a canvas-based environment with live theorem-prover feedback, is in active development.

The OntoLogic Portal showing a conjecture browser of BFO 2020 modules, a CLIF editor, and a proof receipts panel.
OntoLogic Portal: the conjecture browser, the CLIF editor, and the receipts panel recording format, checker, substrate and verdict. Interface design. The command-line toolset ships today.
The reasoning panel showing prover selection, live verdicts, and the counter-example view for a failed claim.
The reasoning panel. Prover choice, live verdicts, and a counter-example rather than a bare rejection when a claim fails. Interface design.
What do your developers actually receive?

Build-ready libraries in C#, Rust, Go, C++, Java, and Python, not wrappers or stubs, each carrying the entity classes, queries, and validation logic derived from your verified knowledge. Alongside them come the artifacts your auditors and reviewers ask for: proof certificates that can be replayed without Reasonics in the loop, provenance records tying every output back to the knowledge that produced it, and graph schemas the runtime executes against. The standards behind each artifact →

For developers: the compiler pipeline, in depth
Roles

Who Uses TruSpark, and Where They Start

Because the process runs end to end, different people join it at different points, and none of them has to do all of it. Pick a role to see where it starts.

Domain and subject-matter experts

Start at the beginning, describing what their field knows, and can read the results back in plain English without touching any code.

The Result

The Result: Trustworthy, Explainable Software

The question a regulator, an auditor, or a client asks of any AI-enabled system is not whether it performs well on average. It is whether this output, in this context, was correct, and whether that can be shown.

TruSpark answers that before the software ships, never after. The knowledge is defined, proven, and turned into software from the proof itself, so every result traces back to the knowledge that produced it. That is what it means to build on a formal knowledge foundation and not approximate one.

It also changes who can check the work. Because every result is generated from formal knowledge, that knowledge can be read back in plain language, so the people who have to sign off on a decision can review the rule itself, instead of taking an engineer's word for what the system does.

OntoVerba™ — English and the Formula, One Tree

Plain language and formal logic are two readings of the same proved statement, so the summary an executive reads cannot quietly diverge from the rule the software enforces.

No drift by construction, both readings come from the same tree
Controlled English
executive · analyst · ontologist · tooltip
← GENERATED FROM →
GlossTree
one tree · one fingerprint
The formal formula
CLIF ·. The verbatim logic

And it runs backwards: controlled English parses back into a tree, which is how someone who does not write logic can still author it.

Read

Ask for the same statement at any level — executive, analyst, ontologist, or a tooltip, and get a faithful rendering, never a loose paraphrase.

registers + personas
How it works

Every rendering is generated from the same tree and carries the same fingerprint, so the executive summary and the ontologist reading are provably the same statement. Registers set the reading level; personas tune the voice for a given audience.

Mint(register, tree)
MintPersona(persona, tree)
GlossModal(register, modal)
Author, the inverse

Write in controlled English and it parses back into formal logic, a fourth way into the platform for people who do not write logic.

today: the controlled register, round-trip proved
How it works

English parses back to a tree, making controlled English the platform’s fourth CLIF authoring channel alongside the AST DSL, the format translators, and the VDL. Failures come back as structured parse errors that point at the phrase responsible, not as silent misreadings.

Author(register, controlled)
→ Result<Gloss, ParseError>
Explain & repair

Ask why a conclusion holds and get the reasoning narrated. When something fails, you are told what to change.

only the prover confirms the edit settles it
How it works

Explanations name the load-bearing axioms, the ones the conclusion actually depends on, rather than dumping the whole proof. On failure the platform proposes the edit: a ranked retraction set, or the assertion that would close the gap. The suggestion is only ever a proposal. The theorem prover confirms whether it settles the question.

ExplainWhy(goal, loadBearing)
ExplainFailure(reg, failure)
RepairFailure(reg, failure)
Teach & document

Meet a newcomer at their level and climb from there, so expertise transfers instead of staying locked in a few heads.

the skill-closing surface
How it works

Teaching works as a ladder: each rung carries the identical fingerprint, so every step up is provably meaning-preserving and not a fresh simplification that may drift. Documentation falls out of the same mechanism, a knowledge corpus documents itself, and CorpusGen turns it into verified training sets for machine learning.

Proof-gated drafting — how a language model is made safe here

A language model can help draft the wording, but it never gets the last word: nothing reaches a reader unless it parses back to the same logic it came from.

Deterministic baseline
A model proposes
shown controlled text, never fluent
Round-trip verify
must re-parse to the same tree
Accept. It surfaces
Otherwise fall back to the baseline
an unfaithful model can never surface a sentence
How it works

The engine stays pure and ahead-of-time safe: the model call lives in a delegate outside the assembly, and with no model wired the deterministic baseline is returned unchanged, so the feature is air-gapped by default. The verifier in place today is the controlled round-trip. A fluent-English back-translator and an entailment check are later phases.

The English and the logic come off the same tree, so neither can move without the other.

Powered by OntoMotion™
See how that trust is built — Architecture & Standards
Next Step

See the pipeline run on knowledge from your own domain.

Request a Demo