Principia
One continuous digital thread
Change a requirement.
Watch it ripple to the twin.
Requirements, architecture, simulation, assurance and verification are one linked model — so change-impact analysis is a query, not a meeting.
- Requirements satisfy · derive
- Architecture parts · ports
- Simulation Modelica · FMU
- Assurance GSN · CAE
- Verification Dafny · FDR · Isabelle
- Digital twin live telemetry
Arrange a pilot See the full walkthrough
- 95+
- SysML v2 meta types
- 9
- languages, one model
- 8.31M
- lines of code
The problem
Documents can't tell you what a change breaks
No shared representation
Requirements, architecture and analysis live in natural-language documents that no tool can check against each other.
Information silos
Each discipline's tool holds its own version of the truth, and none of them interoperate.
Change is untraceable
Impact analysis becomes a series of meetings, and the answer is only as good as who remembered what.
The platform
Nine capabilities, one environment
Browser-native SaaS
Cloud-deployed, zero client install, hot upgrades, identical on Windows, macOS and Linux.
Full SysML v2
95+ metamodel types with bidirectional graphical and textual editing over the standard library.
V-model lifecycle
Requirements, design, simulation, verification and operations as visual project phases.
Deep model management
Epsilon query, validation, transformation and generation — well beyond CRUD.
Real-time collaboration
Concurrent editing with cursor tracking and element-level version control.
Executable trace links
One click opens the target editor; requirement changes surface affected artefacts.
AI4Engineering
Multi-agent LLM assistance generating models from natural-language requirements.
Digital thread and twin
Lifecycle-wide continuity, with 3D assets bound to the live model.
Simulation binding
SysML parameters mapped one-to-one onto Modelica and FMU variables, synced on demand.
Languages and standards
Nine languages, one model
Modelling
- SysML v2 — 95+ meta types, ~82-file standard library, bidirectional graphical and textual
- Ecore/EMF — metamodel editor with auto-generated editors
- GSN 3.0 — modular assurance arguments
- CAE 1.0 / SACM — claims, arguments and evidence
- Modelica — OpenModelica plus FMU co-simulation
- Custom DSL — a metamodel in, a Vue 3 editor out
Formal
- CSP — CSPm, trace and failures refinement checked by FDR
- Dafny — proof obligations discharged on the model
- Isabelle/HOL — theorem proving on an Isabelle2023-CyPhyAssure build
How it compares
Four toolchains, or one platform
The usual stack is an architecture tool, a simulation tool, an assurance tool and a proof assistant — each strong in its own domain, and joined to the others by export, by hand, and by spreadsheet. Principia covers all four, which is what makes the last three rows possible at all.
Scroll the table horizontally →
| Architecture tool | Simulation tool | Assurance tool | Proof assistant | Principia | |
|---|---|---|---|---|---|
| SysML v2 system model | yes | no | no | no | yes |
| Modelica and FMU simulation | no | yes | no | no | yes |
| GSN, CAE and SACM argument | no | no | yes | no | yes |
| CSP, Dafny and Isabelle proof | no | no | no | yes | yes |
| SysML parameters bound to simulation variables | no | no | no | no | yes |
| Trace links spanning all four domains | no | no | no | no | yes |
| Proof results re-run as assurance evidence | no | no | no | no | yes |
Compared by category rather than by product. Individual vendors ship and change capabilities quickly, and a cell-by-cell product table is stale the month it is published.
Where most toolchains stop
Machine-checked proof, wired into the safety argument
Refinement checked in FDR, proof obligations discharged in Dafny, theorems proved in Isabelle/HOL — and the results land as evidence attached to GSN Solution nodes. Re-run the evidence in one click and each Solution is marked sound or problematic. A closed loop from proof to certifiable argument.
CSP and FDR
Trace and failures refinement over the behavioural model.
Dafny
Proof obligations on the implementation, verified with inline feedback.
Isabelle/HOL
Theorem proving on an Isabelle2023-CyPhyAssure build.
Evidence, re-run
Every GSN Solution carries executable evidence, checked on demand.
Simulation binding
SysML parameters, bound to simulation variables
Map a SysML attribute one-to-one onto an OpenModelica or FMU variable and sync them on demand. Design intent and simulated behaviour stop drifting apart, because they are the same number.
Executable trace links
A link you can follow, not a spreadsheet row
Create a link from any element to any other, across any two modelling languages, and clicking it opens the target editor on the target element. Change a requirement and the affected design, simulation and argument surface automatically.
AI4Engineering
From a requirement sentence to a first model
Multi-agent LLM assistance generates system design, Modelica simulation, FMEA and FTA, GSN and SACM argument, traceability and digital-twin models from natural-language requirements. Works with hosted models including Claude, ChatGPT and DeepSeek, or a domain model deployed in-house.
Pilots and partnerships
Put it on a real system
Principia is a mature platform seeking pilot deployments and design partners. If you are carrying a complex system through certification and the toolchain is fighting you, we should talk.
Arrange a pilot Research collaboration
Related work at github.com/wrwei.