Login
Terms and Conditions and LicencesPrivacy Policy
FIPS 140-3
Common Criteria EAL5+

Products

  • ProvenHSM
  • Qualified Signature Creation Device (QSCD)
  • Software Developer Kit (SDK)
  • Security Applications
  • ProvenCore OS and TEE

Use Cases

  • Data Protection
  • PQC Migration
  • Key Management & Cloud KMS
  • Confidential Computing
  • Finance Innovation
  • eIDAS Signature and Identity Wallet
  • Multi-Party Computation (MPC)

Resources

  • Blog and Whitepapers
  • Security and Certifications
  • Integrations

Company

  • Careers
  • About

In this article :

  • The Looming "Verification Gap"
  • The Shift to Mathematical Proof
  • A New Era of Engineering

When AI Writes the World's Software, Who Verifies It?

The rewriting of the global software landscape is no longer a future prediction; it is an active transformation. Tech giants like Google and Microsoft now report that over 30% of their new code is generated by AI. Some industry leaders, including Microsoft’s leadership, predict that by 2030, as much as 95% of all code will be written by AI agents. 

A landmark experiment in February 2026 proved how fast this is happening: a team of 16 parallel AI agents built a functional, 100,000-line C compiler in just two weeks for less than $20,000.

This compiler is capable of building bootable Linux kernels and complex systems like SQLite and PostgreSQL, however, as AI accelerates software production, a critical question remains: Who is verifying the result? 


The Looming "Verification Gap" 


Legacy defenses like code review and manual testing were designed for a human pace of production. They are unsuited for the volume and speed of AI-generated "workslop." 

  • Security Risks: Half of AI-generated code fails basic security tests, and larger models have not yet proven to produce significantly more secure code. 
  • The Heartbleed Warning: A single human error in OpenSSL (Heartbleed) exposed millions and cost the industry hundreds of millions of dollars. AI is now generating similar layers of code at a thousand times the speed. 
  • Reviewer Fatigue: Leading engineers have noted that when AI code is "good enough" most of the time, humans stop reviewing diffs carefully, leading to a loss of oversight. 


The Shift to Mathematical Proof 


At ProvenRun, we believe the answer is not to slow AI down, but to replace human friction with mathematical friction. Testing provides confidence, but formal verification provides a guarantee. 

  • ProvenCore-M & ProvenHSM: By using platforms like Lean or our own Smart language, we move from "marketing trust" to mathematical proof. 
  • Formal Specifications: A proof cannot be "gamed" by an AI over-fitting to a test suite; it covers every possible input and edge case by construction. 
  • Compositional Security: Verified components can be composed with total confidence, ensuring that integration—the place where most bugs live, is sound by design. 


A New Era of Engineering 

As AI takes over implementation, the core of engineering shifts to specification. Writing a precise description of what software must do forces clear thinking and creates a machine-checked defense against AI errors. 

Companies like AWS and Microsoft are already using this approach to verify cryptographic libraries and authorization engines, collapsing years of qualification effort into weeks.  

The goal is a Verified Stack: an open-source, mathematically guaranteed foundation for the digital world. Verification isn't a cost, it’s the catalyst for an AI-driven world that is provably secure. 

Explore ProvenHSM
Bull Logo
Safran Logo
BMW Logo
DGA Logo
Atos Logo
Renault Logo
Microsoft Logo
Orange Logo
OVH Cloud Logo
ST Microelectronics Logo
Bull Logo
Safran Logo
BMW Logo
DGA Logo
Atos Logo
Renault Logo
Microsoft Logo
Orange Logo
OVH Cloud Logo
ST Microelectronics Logo
Bull Logo
Safran Logo
BMW Logo
DGA Logo
Atos Logo
Renault Logo
Microsoft Logo
Orange Logo
OVH Cloud Logo
ST Microelectronics Logo