Trusted products and services for embedded security. Join-us on Linkedin


An ultra-secure Operating System

ProvenCore stands at the core of ProvenRun’s offering of Trusted Computing Base (TCB) secure components. 

Hosting the security critical services

The TCB always includes critical security services that need to remain small and simple to remain verifiable, especially on complex hardware such as modern microprocessors or microcontrollers. Implementing these security functions require high-level abstractions of the hardware, typically provided by an Operating System (OS). Because the correctness of the security functions depends on the correctness of these high-level abstractions, the OS that implements them is also part of the TCB and should be free from exploitable vulnerabilities. 

The implementation of a secure OS is inevitably complex, traditional software development methods systematically fall short of eliminating vulnerabilities that are exploitable by attackers ready to invest a few million dollars. Such investments may seem high, but they are in fact extremely attractive in IoT or CPS settings when put in perspective with the number of devices that can be attacked at the same time, and the damage that can be done by devices that control physical systems. The secure OS needs to be of the highest software quality as possible and be as close as possible to zero defect. To meet that goal, the only available strategy to date is to develop the OS using deductive formal methods. 

Why ProvenCore

ProvenCore is an ultra secure OS developed using deductive formal methods. It is a key milestone for being able to develop secure-by-design connected devices in many sectors (automotive, railways, aeronautics, energy, industrial, medical, etc.) in a cost-effective way:

A Secure OS is always required

Even when using other security technologies such as Secure Elements or hypervisors, an OS is still required to execute the sensitive security services on complex hardware such as microcontrollers or microprocessors, and this OS has to be secure because it is part of a device’s TCB.

Formally proven

ProvenCore is the very first OS to be formally proven for its complete TCB. This is essential to avoid situations in which hackers will exploit weaknesses in the part of the OS’s TCB that has not been formally proven.

High level API

ProvenCore offers a high abstraction level (POSIX-like) to developers of security services. With ProvenCore, the development of security services becomes simpler and cheaper, leading to more security at a lower cost.

More security, lower cost

ProvenCore is formally proven and can therefore claim superior code quality (as close as possible to zero-defects) leaving almost no attack surface to hackers. Use of formal proofs also promotes a much easier maintainability of the ProvenCore code base, a critical factor for a software component as complex as an OS, and consequently a much-reduced Total Cost of Ownership.


For industries that are subject to certification – or that may be subject to certification in the coming years – ProvenCore brings certainty that certification will be achieved painlessly, whatever the requirement level, for the lowest possible cost.


ProvenCore has received a Common Criteria EAL7 certification which is the highest level defined by the Common Criteria certification scheme. 

Certification kits are available with ProvenCore. 

Supported hardware

ProvenCore is available for ARM Cortex-A and RISC-V microprocessors.

Please contact us for more details.

Challenge coverage



Security needs to be integrated at the design stage (security-by-design) and embedded in the most effective way wherever it is required in the technical infrastructure. There are many ways to embed security in systems and devices and the selected solution will be the result of a trade-off between cost, security level and performance.

More info
Trusted Computing Base

Trusted Computing Base

Security engineers define the Trusted Computing Base (TCB) as the set of hardware, firmware and software components that are critical to the security of a system. In order to limit the risk of vulnerabilities, the TCB need to be well identified, as small as possible and made-up of components that can be really trusted.

More info

Other Secure Components