The Architecture of Trust

Trustworthy software isn't the product of a single feature. It is built up in layers, each one depending on the one beneath it. This page follows that chain of trust from end to end: from the meaning your organization defines, to the verified software TruSpark™ delivers. Each layer compounds the assurance established by the layer before it.

Trust, Built by Stratification

Select any layer to open its technical detail.

Formal Ontologies

Everything starts with meaning made explicit. A formal ontology defines the concepts, relationships, and rules of your domain precisely, and grounds them in a shared upper-level standard (BFO 2020) so that a term means the same thing across every domain, department, and system that uses it. That shared foundation is what lets knowledge from different parts of the organization work together instead of quietly conflicting, the misalignments that are expensive to discover late and harder still to unwind.

Common Logic

For software to reason about what your organization knows, that knowledge has to be written down in a language precise enough to leave no room for interpretation. Everyday modeling tools keep things simple so they stay fast, but simplifying is exactly what you cannot afford when a single definition carries regulatory or safety weight.

That is why TruSpark writes meaning in Common Logic (CLIF), a mathematical language that captures the full nuance of a regulated domain instead of a stripped-down approximation of it. The relationships, constraints, and rules that make your field what it is come through intact, ready to be proved and not merely stored.

CLIF is itself an international standard — ISO/IEC 24707:2018, so the language your meaning is written in is governed and auditable, not something Reasonics invented and asks you to take on faith.

Automated Theorem Proving

Before any software is generated, the knowledge is submitted to automated theorem provers that check it is internally consistent and that its conclusions genuinely follow. This is proof, not testing, and a result that cannot be proved is reported honestly as indeterminate, never guessed.

TruSpark does not rely on a single prover. It runs a portfolio of automated theorem provers under one interface, because different provers are suited to different kinds of problems, and a result that several independent provers agree on is far more trustworthy than one from any single tool.

See it decide

Pick a formal statement and watch the prover portfolio reach a verdict — proved, or honestly reported as indeterminate.

(forall (s c)
  (if (specifically-depends-on s c)
    (and (exists (t) (and (exists-at s t) (exists-at c t)))
         (forall (t) (if (exists-at s t) (exists-at c t))))))

OntoProver is Reasonics’ own automated theorem prover, built specifically for BFO 2020 ontological reasoning, with its own tableau, resolution and superposition engines, and a native SMT solver: a DPLL(T) core driving five theory solvers. Three of those are BFO-native — mereology, category disjointness and temporal reasoning — alongside the BFO sort lattice and linear arithmetic. It reads and writes SMT-LIB 2.7 across QF_UF, UF, AUFLIA and AUFLIRA. That is the part an off-the-shelf SMT solver cannot supply: a decision procedure that already knows what parthood and disjointness mean. Z3, CVC5, and Vampire are industry-standard provers used by research institutions and verification teams worldwide, each bringing different strengths to the portfolio.

An inconsistent theory is rejected outright. A theory that contains a logical contradiction can prove anything vacuously, so TruSpark refuses to build on one.

For the business, this is the difference between a system whose answers you hope are right and one whose answers you can defend. Because every conclusion is proved before anything is built on it, the software your teams ship carries meaning that has already been checked, so a decision can be explained to a regulator, reproduced by an auditor, and relied on by the people downstream, without anyone having to trust that the logic simply happened to be correct. Correctness stops being a matter of confidence and becomes a matter of record.

(assume h1 (forall ((x Entity)) (=> (continuant x) (exists-at x))))
(step t1 (cl (not (and (continuant a) (not (exists-at a)))))
      :rule resolution :premises (h1))
(step t2 (cl) :rule contradiction :premises (t1))   ; ⊢ consistent

Beyond first-order logic

The core runs on first-order logic in CLIF, but real questions also ask about time, obligation, actions, and exceptions. TruSpark ships logic extensions for those, while holding the same line on genuine proof. Pick a family below to see its members. The tag on each says whether the platform proves it directly today, handles part of it, or hands it to a specialist tool.

The platform answers instantly when it recognizes a known pattern and escalates to the full prover only when it needs to, and when it genuinely cannot decide, it says so honestly instead of guessing.

OntoProver — Answer Fast, or Escalate Honestly

Verification only helps if it is fast enough to live inside a working day. Because the knowledge is anchored to BFO 2020, a great many questions have known answers, so the cheapest tier that can answer, answers, and anything the shortcuts do not genuinely recognize goes to the full prover rather than being waved through.

Tier 1 · Known shapes 1–10 nanoseconds

Questions matching a known BFO pattern are answered from precomputed results, no solver is called at all.

answers are precomputed

How it works

This is the BITS layer — bit-level BFO reasoning. BFO’s fixed relationships are encoded as bit patterns and not as statements to be solved: disjointness matrices, sub-universal lattices, Allen interval tables, clause arenas, and relation counters, shipped pre-saturated as a binary resource. Answering becomes a bitwise lookup instead of a solver call. Roughly 5,500 lines across 19 files.

→ no match

Tier 2 · Known theory Microseconds

If every axiom in a module is a recognized BFO 2020 theorem, the module is certified consistent without ever invoking the prover.

structural identity, not heuristics

How it works

A fast-path matcher checks axioms against a catalogue of top-level ontology theorems by structural identity, not by similarity scoring, so a near-match is a miss instead of a guess. One shared adapter means the layer fires identically on every route into the prover.

→ no match

Tier 3 · The full prover Full saturation

Anything unrecognized is declared out of scope and handed to the full theorem provers. Nothing is approximated to look fast.

a timeout is never reported as a disproof

How it works

Unrecognized conjectures are dispatched to the saturation engine — OntoProver alongside Z3, CVC5, and Vampire. Verdicts stay three-valued: proved, disproved, or indeterminate, so a timeout is reported as unknown rather than quietly counted as a refutation.

What counts as a recognized shape

Sub-universal — anything that is an instance of the narrower kind is also an instance of the broader one

Inverse relation , both plain and time-indexed forms of a relation and its converse

Disjointness , two kinds that cannot share an instance

Counter-model goal , a claim that something belongs to two disjoint kinds at once — refutable by construction

How it works

Matching is structural. A refutation requires a shared witness variable and temporal index — distinct witnesses are satisfiable and fall through to the next tier instead of being reported as a contradiction. The shapes follow the BFO 2020 corpus anti-conjecture form, expressed in CLIF as (forall (t x) (if (instance-of x SUB t) (instance-of x SUPER t))) and its relatives.

Where the same discipline reaches

The same escalate-honestly rule governs transaction logic, dependent type theory through Lean 4, and the native bindings your developers call from Rust, Go, C++, and Java.

speed figures are internal benchmarks, not published results

Most questions never reach the prover. The ones that do are not hurried.

Powered by OntoMotion™

Compiler Architecture

Once a theory is proved, TruSpark compiles it into executable software. Compilation is gated on verification: a build that succeeds but contains anything that does not match its proved source is treated as a defect, not a release.

Reasonics calls this principle verification-first emission. Every artifact emitted, in every language, across every deployment target — carries the same machine-checked semantics and an independently replayable proof certificate. It is the difference between trusting software because you read its documentation and trusting it because a machine proved its claims.

Proof Certificates

Every proof produces a certificate, a portable, machine-checkable record of exactly how a conclusion was reached. You do not have to take Reasonics’ word for it: a certificate can be replayed in an independent checker, with TruSpark nowhere in the loop.

Certificates are emitted in three independently verifiable formats — TSTP, Alethe, and SMT-LIB 2.7.

By the numbers

Each figure carries its own evidence. Click a stat to see exactly what it measures — and, just as important, what it doesn’t.

Polyglot SDKs & Generated Outputs

Finally, the verified core is delivered into your environment as build-ready software your teams can use directly, in the languages they already work in, with the evidence from the layers above traveling alongside it. The assurance built up across the previous five layers arrives as something your teams can ship, never a report someone still has to act on.

Where to next

Have your architects put the standards and the proof trail under scrutiny.