Why a Formal-Verification Software Company Built an HSM

People who know ProvenRun know us as a software company — and a fairly extreme one. We build operating systems whose security properties are established by mathematical proof, not by testing alone. In 2019, ProvenCore became the first OS of its kind to achieve Common Criteria EAL7, the highest assurance level in the framework. Our code runs deep inside connected vehicles, industrial systems, and defense platforms, in the layers most users never see.

So when we tell people our flagship product is now a 1U network appliance you rack in a datacenter, we get a fair question: why would formal-methods specialists in embedded software go into cloud hardware?

The short answer: because the hardware security module is where our software matters most — and where the industry's need for it is most visible.

Assurance Has a Market Price, and the HSM Sets It

For most of the software industry, assurance is a virtue. In the HSM market, it is the product. Organizations buy HSMs precisely because a certificate — FIPS 140-3, Common Criteria — attests that the device protecting their keys resists attackers. It is one of the few markets where customers explicitly pay for proven security rather than promised security.

That should have made the HSM the natural home of formal verification years ago. Instead, the category froze. Even a competitor's CEO recently wrote in Forbes that the traditional HSM "hasn't changed much in decades, even as everything else around it has" [— link to source] — reliable, but a box: manually provisioned, hard to integrate, slow to scale, expensive to evolve. The diagnosis is now shared across the industry. The disagreement is about the cure.

The Certification Dilemma Is a Software Problem

Here is the mechanism that froze the category. An HSM's value rests on its certification, and certification traditionally evaluates the device as a monolith. Change anything — add an algorithm, a feature, a customer application — and you risk reopening the entire evaluation: months to years of delay and significant cost. So vendors change as little as possible, and innovation moves at the pace of recertification. Customers get security or velocity, never both.

This is not fundamentally a hardware problem. It is a software architecture problem, and it happens to be the exact problem we spent fifteen years solving.

ProvenCore's formal verification does more than establish the absence of runtime errors. It proves isolation and compositionality: the guarantee that components running on the kernel cannot interfere with one another, mathematically, not merely by configuration. When isolation is proven at that level, an evaluator can reason about components independently. A new trusted application does not invalidate the certified foundation. Certification becomes incremental — a delta on what changed, like the smart-card industry has long practiced — instead of a restart.

That single property dissolves the HSM's core dilemma. You can have a stable certified core and a platform that evolves in weeks. But you can only deliver the property end-to-end if you control the full stack: kernel, runtime, crypto, and the hardware boundary it all runs in. That is why we built the box.

Why Hardware, and Why Cloud-Operated?

We could have licensed the technology and stopped there — it is, after all, our historical model. Two forces pushed us further.

First, trust needs a boundary you can point to. Sovereignty requirements in Europe, HYOK and key-control mandates in the cloud, eIDAS obligations for qualified trust services — all of them ultimately ask the same question: where exactly are the keys, and who can touch them? A formally verified software stack deserves a hardware root of trust with tamper protection, attestation, and a defense-grade supply chain. Designed and made in France, auditable by any trusted authority, with the complete certification evidence — source code included — available to customers who need to verify rather than believe.

Second, the operational model had to be the opposite of the legacy experience. The datacenter ceremony — flying people in to stand in front of a box with tokens and smart cards — belongs to another era. ProvenHSM ships from the factory to the installation site and everything after that is remote: deployment, administration, backup, recovery, updates, all over REST APIs and mTLS, with M-of-N quorum and role-based control for sensitive operations. Cloud-native operations on customer-held hardware: that combination is the point.

The Same Company, One Layer Up

Seen from the inside, this is not a pivot. It is the same conviction applied at a new altitude: that the only security claims worth making are the ones you can prove. We proved an OS. Now we are proving a platform — one where our customers' own applications inherit the guarantees, through the SDK, the simulator, and delta-certification paths.

The HSM is where we start, because it is where proof is already valued. Where it leads — programmable trust for identities, transactions, and increasingly autonomous systems — is a story for another post.