Proofcraft News - 2025

Gerwin presents the next 700 verified seL4 platforms at the seL4 summit

Proofcraft’s Chief Scientist Gerwin Klein presented at this year’s seL4 summit held in Prague, Czech Republic on September 3rd 2025, where Proofcraft was a Silver sponsor.

In his talk (soon to appear on seL4’s Youtube channel), Gerwin shared exciting news: in the next seL4 release, the formal proofs for seL4 will cover 100% of the Arm platforms it supports.

In the same project, which is part of the DARPA’s PROVERS program, Proofcraft is also investigating how to extend the proofs to a larger number of configuration options. If successful, this could expand the configuration space the proofs apply for to over a trillion different individual option combinations.

seL4 proofs now supported on 100% of Arm platforms that the kernel can run on

seL4 can run on 22 different Arm platforms. As of last year, seL4 was verified for only 3 of these platforms. Now, the formal proof covers 100% of the Arm platforms that seL4 supports. Recently, a 23rd Arm platform was added to the supported list, and remarkably, the proof for this new addition required zero new work.

This progress is part of Proofcraft’s initiative to reduce reliance on experts, as part of DARPA’s PROVERS program. By automating the verification of seL4 for new hardware platforms, engineers can use a verified configuration of seL4 across a growing array of platforms without the need for Formal Methods expertise.

Looking ahead, the next goal is to extend this kind of proof support to all RISC-V platforms that seL4 runs on, as well as to the large number of configuration options that seL4 supports.

Proofcraft Silver sponsor of the seL4 summit 2025

Proofcraft is proud to be sponsoring the 2025 seL4 summit as a Silver sponsor.

The seL4 summit is an annual international gathering of participants from industry, government and universities with interests in the world’s most highly assured OS kernel. Attendees and presenters include the creators and maintainers of the seL4 technology such as the Proofcraft team.

This year’s seL4 summit will be held in Prague, Czech Republic, on Sep 3-5, 2025.

Proof that seL4 enforces integrity. Now also on AArch64.

The verification of seL4 on the 64-bit Arm architecture continues at Proofcraft, thanks to continued support from NCSC. After completing the proof of functional correctness, Proofcraft has now established the proof that seL4 enforces integrity on AArch64, providing a formal mathematical proof that the kernel prevents an application running on top of seL4 from modifying data without authorisation. For the first time in seL4’s security theorems, this includes hypervisor mode and FPU support. Next on the roadmap is the proof of confidentiality: that an application is prevented from learning information from other applications without explicit authorisation.

4 years since the creation of Proofcraft

Proofcraft is celebrating its 4th year anniversary, still enjoying pushing the limits of verified software, with multiple multi-year projects started in the last year!

Pushing the availability and ability to use verified software for non-experts, in DARPA’s PROVERS program. Pushing verified software in areas where using multiple processors is imperative for high performance, in Cyberagentur’s ÖvIT program. And continuing to push the verification of seL4 on AArch64 with further funding from NCSC.

Many exciting developments to come.

Proofcraft recipient of Cyberagentur funding for verification of seL4 multikernel

Proofcraft, partnering with Kry10, is one of the 5 recipients of Germany’s Cyberagentur’s Ecosystem trustworthy IT research program (ÖvIT).

Kry10 and Proofcraft partner to deliver dynamism, performance, and proof for complex cyber-physical systems. The project will enable: over-the-air updates using dynamic configurations; high performance using multiple cores; and high security assurance using rigorous design and formal verification.

In particular, Proofcraft will extend the seL4 microkernel proofs to support a static multikernel configuration, where applications can benefit from the use of multiple CPU cores for performance, while at the kernel level a separate instance of seL4 run on each core.

At ÖvIT kick-off meeting on January 20th, 2025, at Leopoldina National Academy of Sciences in Halle (Saale) Germany, June Andronick presented Proofcraft’s contribution to the program, together with Matthew Brecknell from Kry10, while Boyd Multerer, CEO of Kry10, presented the vision for the whole project.