Proofcraft News - 2026

Proofcraft presenting at the Cyberagentur Milestone Research summit

In April 2026, Germany’s Cyberagentur held a Milestone Research summit to present the progress and outcomes of its funded programs, including the Ecosystem trustworthy IT research program (ÖvIT), which Proofcraft is a recipient of, partnering with Kry10.

Proofcraft’s Chief Scientist Gerwin and Kry10’s Chief Scientist Martin Dehnel-Wild presented the progress on the Dyvercon project, to deliver dynamism, performance, and proof for complex cyber-physical systems. In particular, Gerwin reported on Proofcraft’s work on extending the seL4 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.

Gerwin additionally gave a general introduction to formal verification and overview of its use in the real world.

Proofcraft is a proud sponsor of the seL4 summit 2026

Proofcraft is happy to be supporting the 2026 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 Vancouver, Canada, on Sep 1-3, 2026.

5 years of Proofcraft. 5 years closer to a verified future.

On the 14th of April 2021, we created Proofcraft. Five years later, we are so busy working for a verified future that we have not posted news for a while.

Much has happened, and more is to come. For now, here are some posts from our back log of news items with technical highlights that Proofcraft has been delivering.

Firstly, the seL4 proofs are now supported on 100% of Arm platforms that the kernel can run on. With this significant progress towards reducing the reliance on experts, users of seL4 can now choose freely between the supported Arm platforms and always be sure they use a verified code base. This work is part of DARPA’s PROVERS program.

Secondly, seL4 on AArch64 now provably enforces integrity: We have a formal mathematical proof that the kernel prevents an application running on top of seL4 from modifying data without authorisation. And the work on security theorems goes on: thanks to continued support from NCSC, we are close to completing the confidentiality property, and with that the entire security proof stack for the 64-bit Arm architecture.

Much more is happening, with three large projects going on in parallel, funded by DARPA, Cyberagentur and NCSC respectively. Stay tuned for more!