Fits Your CI/CD Pipeline
TruSpark is driven by a command-line tool, ontoenactc, and a batch build engine that your pipeline calls like any other step. There is no new platform for your team to operate and no separate console to babysit, the same automated build that already compiles and tests your software also compiles your knowledge and generates the SDKs from it.
The benefit is that verification stops being a ceremony anyone has to remember. The proof gate runs as a build step: if the formal theory does not prove, the build fails, exactly like a failing test, and nothing unproven ever reaches production. Correctness becomes something your pipeline enforces automatically on every commit, using tools your developers already know, instead of a manual review that depends on discipline.
The whole platform, from a shell
Everything TruSpark does is available as a command-line tool and a batch build engine, so verification runs inside the pipeline you already have, on your own infrastructure, with no console to log into and no network call required.
How it works
The build engine sits behind the command-line tool and drives SDK generation across ontologies and languages under the proof gate. Each build is itself a verified workflow — checked before it runs and audited while it runs. A failing proof stops the emit. It does not warn and continue.
Twenty-nine command groups cover the platform, and the engine can also be called programmatically where a team wants to drive builds from its own tooling. Air-gapped environments are supported: nothing in the build path requires an outbound connection.
Working Alongside Your Systems of Record
One of the persistent challenges in enterprise software is getting systems that were built independently to mean the same thing. An adverse event in a clinical trial management system, a safety signal in a pharmacovigilance platform, and a regulatory submission record may all refer to the same real-world occurrence, but unless those systems share a formal definition of what that occurrence is, connecting them requires manual mapping work that must be redone every time either system changes.
TruSpark addresses this at the foundation. When systems are built from, or aligned to, the same formally verified knowledge layer, their outputs are semantically consistent by construction. The concepts they work with carry the same formal definition, the same relationships, and the same rules. Data moving between systems does not need to be manually reconciled because the meaning was agreed upon before the first line of code was written.
This is not a mapping layer added between systems after the fact. It is a shared definition of what things mean, compiled into the systems themselves, so integration is a consequence of how the software was built, not a problem to solve once it is running.
And what you already run stays exactly where it is, open any item for detail:
Validated systems
EDC platforms, CTMS, regulatory submission tools, ERP systems, compliance platforms, and any other validated or certified systems in the environment. TruSpark adds a knowledge foundation alongside them, not between them and their data.
Development tooling
Existing CI/CD pipelines, source control, build systems, and testing frameworks. TruSpark's compiled output integrates with standard build systems in each language: MSBuild for C#, Cargo for Rust, Go Modules for Go, CMake for C++, Maven for Java, and standard packaging for Python.
Deployment environments
On-premises servers, cloud infrastructure, edge devices, embedded systems. TruSpark's compiled output runs wherever the target language runs. There is no TruSpark runtime requirement on the deployment target.
Existing AI infrastructure
LLMs, agentic frameworks, and probabilistic AI systems remain in place. TruSpark operates as a knowledge foundation that makes the outputs of those systems more reliable, never as a replacement for them, organizations that have already invested in AI add formal verification and explainability rather than starting over.
Existing graph databases
Neo4j, TigerGraph, and similar graph database infrastructure stay in place. TruSpark's runtime graph engine adds a formally verified ontological layer alongside existing graph infrastructure, not instead of it. See Architecture & Standards for how it differs from a graph database.
At deployment, none of your enterprise data moves into TruSpark. Your records stay in the systems that already hold them, and TruSpark reads and aligns meaning across those systems without taking custody of the data itself. The formal knowledge you define and the software TruSpark generates from it remain your organization's property, and both can be exported in open, standards-conformant formats at any time. Nothing about running TruSpark requires surrendering ownership of your data or your knowledge.
Ways to Deploy
TruSpark reaches every architecture through four deployment surfaces, from in-process embedding to AI-agent integration. The right surface depends on the environment and use case, and more than one can be used together.
Four deployment surfaces, one TruSpark core.
The compiled output then runs across the full range of environments where real-world systems operate. A single verified ontology compiles to native code in six languages, and that code runs wherever those languages run, open any target for detail.
Enterprise software
C#, Java and Python SDKs integrate directly with enterprise application stacks, ERP systems, compliance platforms, and cloud services.
Cloud infrastructure
All six language SDKs deploy to standard cloud environments. The gRPC deployment surface supports microservice architectures and distributed systems.
Edge and IoT devices
The NativeAOT FFI produces a C-callable shared library with no runtime dependency. Connected devices, industrial sensors, and IoT infrastructure receive the same formally verified knowledge as enterprise systems, with no compromise on correctness.
Embedded systems and firmware
For environments where runtime overhead is measured in microseconds, the NativeAOT FFI eliminates the managed runtime entirely. Safety-critical systems get formally verified knowledge at bare-metal performance.
Medical devices
Wearables, implantables, and diagnostic equipment that generate clinical data can be formally aligned with trial data standards and regulatory submission requirements through TruSpark-compiled knowledge, without manual reconciliation.
Licensing and Entitlements
Every TruSpark platform technology is governed through licensing and entitlements, enforced as formally verified knowledge and not configuration flags. Your entitlements determine which capabilities, SDKs, reasoners, languages, deployment targets, and runtime options your organization is provisioned to use, resolved per-feature at load time so what runs in your environment always stays under your governance and matches exactly what you have adopted. Enforcement is machine-bound: entitlements travel as signed, node-locked tokens that are verified at runtime and fail closed, so an unprovisioned capability cannot execute even when its binaries are present.
The same substrate protects what you build on TruSpark: the SDKs you generate, the formal knowledge and taxonomies you author, and the applications you build on top remain your property, governed by the same formally verified licensing layer that governs TruSpark itself.
Security and audit detail (for technical evaluators)
Every translation and verification step produces a SHA-256 hash-chained audit trail, and the origin of every axiom is recoverable from the artifact alone. Proof artifacts persist in independently replayable formats — Alethe, SMT-LIB, TSTP, each addressable by a stable identifier for archiving, transport, and replay without TruSpark in the loop. Access is governed through Ed25519 machine-bound tokens with AES-256-GCM-sealed payloads; Enforcement today is embedded and single-node, and it fails closed. Fleet-wide state such as seat leases and revocation across multiple nodes is on the roadmap instead of shipping; its revocation store is designed to read conservatively, returning “revoked” under uncertainty rather than granting access it cannot confirm. What is available now and what is still in development is listed in full on Products → Platform availability.
Building Your Team's Self-Reliance
TruSpark is designed to transfer capability to your organization, not create a dependency on Reasonics. That objective shapes the whole platform.
The SDK-based architecture means your internal development teams build and maintain TruSpark-based applications without specialist involvement for every change. When a regulation updates or a protocol changes, the formal knowledge layer is updated and the software regenerates automatically, no outside support required, no re-engineering cycle.
The goal is an organization that understands its own formal knowledge, can extend it as requirements evolve, and does not depend on outside involvement to keep its software current. Professional services that never end are not a foundation. They are a dependency, and TruSpark is built to avoid creating one.
Developers keep working in familiar languages, IDEs, and pipelines, taking on ontology-driven development one step at a time. Reasonics supports that learning curve at every stage:
Guided platform experiences
Interactive consoles let a team explore the live ontology and watch formal reasoning happen before writing a line of code.
Documentation and technical references
Complete references for the SDKs, APIs, formats, and deployment surfaces your teams build against.
Tutorials and learning resources
Step-by-step material that builds ontology-driven development skills incrementally, at the team's own pace.
Formal training
Structured training that brings engineers and domain experts up to speed on authoring, compiling, and consuming formal knowledge.
Expert implementation guidance
Reasonics works directly alongside your team during onboarding and the first builds, transferring capability instead of retaining it.
Ongoing customer success
Continued support as your formal knowledge, applications, and requirements evolve over time.