Proofcraft ha cerrado la demostración matemática de que el microkernel seL4, en su implementación para AArch64 (ARM de 64 bits), preserva la confidencialidad de los datos. Con las pruebas previas de corrección funcional e integridad ya finalizadas, la empresa culmina así la pila completa de garantías de seguridad para esa arquitectura, un trabajo respaldado por el NCSC británico. El aislamiento verificado impide que un ataque a aplicaciones no críticas pueda propagarse hacia aplicaciones críticas.
En el frente de arquitecturas, Proofcraft demostró también la corrección funcional del seL4 en su configuración MCS (Mixed Criticality Systems) sobre RISC-V, el mayor añadido reciente al kernel, pensado para sistemas de tiempo real en automoción. La prueba se portará ahora a ARM de 64 bits en el marco del programa PROVERS de DARPA.
La compañía introdujo además, en seL4 15.0.0, una nueva API que admite cargar calendarios de dominio semi-estáticos en tiempo de ejecución, lo que flexibiliza la aplicación del control de flujo de información y facilita el desarrollo con SDK tipo Microkit. En el plano teórico, la empresa contribuyó a un artículo sobre álgebra de construcciones iterativas, presentado en el 41º simposio LICS en Lisboa y aplicable a asistentes de demostración como Isabelle/HOL.
Proofcraft también expuso sus avances sobre configuraciones multikernel estáticas en el proyecto Dyvercon (junto a Kry10, financiado por la Cyberagentur alemana), patrocinó como Silver el seL4 Summit 2026 de Vancouver y su CEO, June Andronick, ofreció una keynote en la conferencia de primavera del CDIS en Estocolmo. La compañía celebra su quinto aniversario.