Use Cases

Formal Verification

Building a foundation based on formal verification enables us to precisely define with a formal model what a system can do. This is then matched, through proofs, to the actual code implementing the model. If the proof can satisfy the model, the code is formally verified. Formal verification allows us to establish the correctness of a system to the same degree of confidence that you know that 1 + 1 = 2, eliminating human error. In other words, we have mathematical proof of the BedRock Hypervisor’s effectiveness. At BedRock we are building formal verification at scale by investing in automation.

Minimal Attack Surface

The BedRock Hypervisor combines the best concepts from microkernels, capability-based systems, and modular design for superior performance, security, and isolation. Because it enforces the principle of least authority, BedRock is able to guarantee that most attacks are not possible to begin with. Our secure architecture keeps all critical functions, including Active Security and Policy Enforcement, below the OS-reachable attack surface, thereby fully protecting the OS and its applications.


BedRock Security is enabled without a cooperating operating system or application, eliminating the attack surface of the components. Based on formal verification, the capability-based system ensures resources can only be accessed when explicitly enabled. With this level of security embedded into the BedRock Hypervisor, users can run the software stack from the OS and up without modification beyond their life cycle, while still preventing attacks.

Unmodified Guest OS & Applications

The BedRock Hypervisor is designed to run unmodified guest operating systems without the need to recompile the kernel or any application. Powered by formal methods, the Hypervisor cannot be breached, and, therefore, is not part of the attack vector. The fundamental hardware abstraction layer can leverage hardware features while concealing them from the OS, increasing system security.


No Vendor Lock-In

The BedRock Hypervisor includes a business-friendly open source license. This prevents vendor lock-in, provides freedom of choice, and prohibits intellectual property contamination. Rather than create a dependency, BedRock Systems is committed to community-driven projects and collaboration.

BedRock Systems believes that computing should be built on a rock-solid foundation. Our BedRock HyperVisor™ (BHV™) provides a trusted computing base with a minimal attack surface that will transform the software foundation from edge devices to the cloud. Based on our Bare Metal Property™ it provides formally verified isolation at a scale that has never before been achieved, combined with BedRock Active Security™, VM introspection, and policy enforcement. BedRock has created a secure layer of protection that is both invisible and un-bypassable, which also enables a rapid adoption of critical workloads, containers and services.

HyperVisor™ & Active Security™


Use Cases

BedRock Embedded™

Give embedded devices the safety and security they require by BedRocking existing hardware. Embedded represents the Intersection of Safety and Security with a formally verified trusted computing base (TCB). Safeguard existing apps and OS by minimizing available attack surfaces with dependable separation proven by the Bare Metal Property™.

For ultra-secure mobile devices, this solution optimizes software defined/SWaP-C and protects critical applications from malicious intent.

BedRock’s Embedded solution is designed for users in defense, Defense Industry Businesses (DIB), government and critical industries.

BedRock Worx™

In the modern work environment, work from home is a fact of life. BedRock Worx provides ultra-secure WFH critical apps. This is not simply App Virtualization for temporary conditions. With Worx, users can leverage existing desktops and realize substantial budget savings vs. creating a complicated and expensive virtual desktop infrastructure (VDI) backend infrastructure.

Worx enables users to BedRock existing hardware for classified/secret applications in an unclassified domain OS.

BedRock Worx provides anti-spy protection with attention management using built-in webcam and secure communication via Secure Enclave.


BedRock Critical™

BedRocked safety and security for the most important systems in critical industry, industrial settings, government, defense industry business (DIB), financial services and healthcare.

SDx/SWAP-C control systems, IPC and servers. With formally verified TCB, BedRock Critical enables SCRM for unmodified consolidated assets.

Achieve cyber resilience SWaP-C and support crucial SCRM initiatives by BedRocking on 64-bit COTS HW.

Supports modernization in the ICS, IIoT & Energy sectors Dynamic policy, separation proven by the Bare Metal Property™.

BedRock Enclave™

BedRock Enclave provides an ultra-secure cloud option for users in government, financial services and healthcare. Enclave protects data from leakage even without a trusted infrastructure.

BedRock the cloud for rich OS and Applications, safeguard the mission algorithm and data:

Protect IP and code and process private data with public algorithms in the cloud.

Cloud and Edge Enclave serves users in settings where privacy is required, like government, financial services, healthcare and in shared cloud infrastructures.

Enclave is silicon independent, based on the BedRock Bare Metal Property™ and Zero Trust Design™.