Deterministic.
Formally verified.
Standards-mapped.
This page is the engineering contract. No marketing, no hand-waving.
Five layers. One trust boundary.
Every command flows top-to-bottom: agent intent, trust scoring, deterministic verification, graph state, capability-gated dispatch. The capability boundary between layers 3 and 5 is the only path to hardware. Agents cannot bypass it.
Each layer can be operated in isolation for unit tests. The kernel is the only layer with a formal correctness argument.
Two paths. One contract.
Pre-compiled deterministic rules evaluated against the live knowledge graph. No solver, no allocations on the hot path.
routed when agent confidence ≥ 0.85 and trust ≥ 0.50
Z3 SMT encoding of joint and velocity constraints, run against an isolated copy of the live graph. A solver timeout rejects the command and steps the cell down to a safe stop. Never fails open.
routed when low confidence or trust < 0.50
Architectural support, not certification.
SafeKernels is not certified against these standards today. The table describes the architectural controls that map to each standard's requirements, and the path to certification.
| Standard | SafeKernels control | Status |
|---|---|---|
| ISO 10218-1:2025 | Capability boundary, audit trail, software safety arguments | Architectural support |
| ISO 10218-2 | Cell-level coordination, mutual exclusion patterns | Architectural support |
| ISO/TS 15066 | Force-and-contact graph patterns align with power-and-force-limiting | Architectural support |
| IEC 61508 | 2-of-3 voting, deterministic kernel, hash-chained audit (SIL 2/3 techniques) | Architectural support |
| ISO 13849-1 | Performance level Pld/Ple control structure mapping | Architectural support |
| IEC 62443 | OT cybersecurity controls | Roadmap |
Each failure has an explicit degradation path.
-
01
Replica crash
Counted as a rejection. Quorum still achievable with two healthy replicas.
-
02
Network partition
Same as a crash. Reject-by-default until the partition heals.
-
03
Z3 timeout
Reject the command and step the cell down to a safe stop. Never fail open.
-
04
Sensor tick lag
Verify against the last-known KG. Threshold-driven degradation if sustained.
-
05
WAL hash break
Detected on the next audit-chain check. The cell drops to a hard E-stop and won't accept a software reset.
-
06
LLM hallucination
Command rejected, trust decrements. After three rejections in ten seconds, the agent loses the fast path; every subsequent command goes through the formal solver.
Adversaries in scope.
| Adversary | Defense |
|---|---|
| Compromised agent | Kernel-mediated verification. Agent cannot call HAL directly. Capability boundary. |
| Compromised vendor controller | Short approval lifetimes, hardware-layer validation, audit-log reconciliation of dispatched vs. received commands. |
| Network MITM (agent ↔ kernel) | Signed approvals. mTLS · Roadmap |
| Rogue operator | RBAC on policy reload and operator-reset. Audit trail in the WAL. |
| Physical tamper with WAL files | Hash-chain detection drops the cell to a hard E-stop. |
Out of scope today: firmware-level compromise of the host running the kernel, side-channel attacks against Z3, hardware supply-chain compromise.
Stress-test the safety argument.
Bring your hardest scenario. We'll walk through fast-path rules, Z3 encoding, and graph patterns end-to-end. See pricing if you're scoping commercials.