Proofcraft News - 2023
# 2023-05-04 - Proofcraft leaders among ACM Software Systems award recipients!
Gerwin, June and Rafal, the 3 founders and leaders of Proofcraft, have received, together with their former colleagues at the Trustworthy Systems group, the prestigious ACM Software System Award, for the “development of the first industrial-strength, high-performance operating system to have been the subject of a complete, mechanically-checked proof of full functional correctness”.
This award, from the Association of Computing Machinery, the world’s largest scientific and educational computing society, recognises the development of a software system that has had a lasting influence, reflected in contributions to concepts, in commercial acceptance, or both.
The award highlights how much seL4 has fundamentally changed the research community’s perception of what formal methods can accomplish: it showed that not only is it possible to complete a formal proof of correctness and security for an industrial-strength operating system but that this can be accomplished without compromising performance or generality. The continuously maintained and growing proofs on seL4 have helped to give rise to a new discipline of proof engineering—the art of proof process modelling, effort estimation, and the systematic treatment of large-scale proofs.
Proofcraft is dedicated to keep pushing the application of formal methods and proof engineering to real-world systems software, increasing its reliability, safety and security.
# 2023-04-14 - Proofcraft celebrates its 2nd anniversary!
People often ask us how things are going at Proofcraft.
As we are celebrating 2 years since we launched this new adventure, we are happy to share that things are looking good! :)
Working at Proofcraft is great and we are having a lot of fun pushing the vision of a verified future.
Our second year has seen us delivering the invariant proofs for seL4 on the latest 64-bit Arm architecture, starting on the design-to-code refinement proof of the Mixed-Criticality-System configuration of seL4, presenting our roadmap for seL4 verification at the seL4 summit, and importantly seeing the Proofcraft family getting bigger with Corey, Michael and Ryan joining!
Amongst other things :)
Looking forward to the years ahead.
# 2023-03-30 - Proofcraft completes the proof that seL4 AArch64 preserves all key invariants
The level of assurance for seL4 on AArch64 is getting stronger.
After having formalised, in March 2022, the abstract specification (what the kernel is supposed to do), and the design specification (how the kernel is designed), Proofcraft has now completed the proof that the abstract specification preserves all key invariants about kernel data structures. This represents a significant proportion of the effort needed to establish the full functional correctness of seL4 on AArch64.
# 2023-02-04 - Listen to Gerwin's interview on Type Theory Forall podcast
Listen to Gerwin talk about his formal verification journey and thoughts on the field, from his PhD on Java Virtual Machine verification and him leading the landmark verification of the seL4 kernel, to creating Proofcraft to provide commercial support in formal verification, and much more. Grab a cup of coffee, or go for a walk with your earphones, or save it for your next flight, and listen to Gerwin sharing his insights, thoughts and anecdotes on this Type Theory Forall podcast.