BERK Hard RT Core — an EAL7-targeting deterministic execution engine
A deterministic execution engine for security- and safety-critical embedded systems: a concurrency design model-checked with TLA+/TLC, HSM integration, an immutable decision journal and WCET-analysed scheduling.
18.4 million states. Zero errors.
The core's concurrency model was specified in TLA+ and explored by the TLC model checker across 18,404,041 states — to a depth of 41, with no errors found.
Proven properties
NoDeadlock, WriteLockExclusive, NoReadWriteConflict, DJRRecordsUnique, DJRVersionMonotonic, ValidAuthorityLevels, TypeInvariant — all machine-checked.
Decision journal (DJR)
An immutable audit trail: every decision is journaled with unique, monotonically versioned records. The DPAL layer — Defensible, Provable, Auditable, Lawful.
HSM integration
Hardware security module support: YubiHSM 2, TPM 2.0 and PKCS#11 — working alongside multi-level authorization (Authority Checker).
Hard real-time
Deterministic scheduling with WCET analysis; deterministic memory via the arena allocator; O(log n) spatial indexing (R-Tree) and tombstone lifecycle management.
Embedded-ready
no_std build target; lock-free concurrency primitives; designed for high operation throughput in defense use cases.
EAL7-targeting
Designed for Common Criteria high-assurance certification. Forms the core of the BerkLink tactical data link product.