Partner with experts to verify your software
Learn formal verification from the experts
Software rules the world.
Does it deserve our trust?
That's what formal verification provides.
That's what we are world experts on.
What Proofcraft can do for you
If you are seeking commercial support, verification projects, training or consulting on formal verification in general or involving the seL4® microkernel specifically, you are in the right place. Send us an email at contact@proofcraft.systems
Interested in enhancing the assurance of your software?
We can deliver contracted projects around verified software in general, and verification of seL4 and seL4-based systems in particular.
Interested in learning more about formal methods or setting up training for your team?
We provide training (online or in person as feasible) on formal verification at various levels of technical depth and for various audiences, from students and individuals wanting to skill-up, to teams of engineers and executive decision makers.
Interested in obtaining expert advice on high-assurance software, including seL4?
We provide consulting on producing trustworthy software through formal verification.
Who is Proofcraft
Our founders are world-famous for applying formal verification to real-world systems software, increasing its reliability, safety and security.
They are experts in mathematical machine-checked software verification, with decades of experience in interactive theorem proving.
They led and contributed to the landmark verification of the seL4® microkernel as part of the Trustworthy Systems group. They are members of the seL4 Foundation board and Technical Steering Committee.
June Andronick
CEO
June has extensive leadership experience towards making the vision of verified software a reality in mainstream critical software. She was previously leading the Trustworthy Systems group, and contributed to the original seL4 verification. She is a Conjoint Professor at UNSW Sydney, Australia. June is also CEO of the seL4 Foundation.
Gerwin Klein
Chief Scientist
Gerwin has a 20-year track record of visionary research with real-world impact. He planned, led, and executed the initial verification of seL4, as well as many of its extensions, and has since been leading its scientific direction. He is chair of the seL4 Foundation Technical Steering Committee and a Conjoint Professor at UNSW Sydney, Australia.
Rafal Kolanski
Chief Engineer
Rafal is a highly skilled and experienced proof engineer. He has a passion for robust engineering practices applied to the field of proof engineering, which he and his team pioneered. He led the seL4 Proof Engineering team within Trustworthy Systems for 5 years and is responsible for many of the modern techniques and mechanisms introduced into the seL4 verification since then. He holds a PhD from UNSW Sydney.
Corey Lewis
Principal Proof Engineer
Corey has years of engineering experience and has contributed to all aspects of the verification of seL4, from maintaining the functional correctness, integrity and confidentiality proofs, to the areas of multicore verification and verified seL4 system initialisation. He has also worked on the verification of the eChronos real-time OS and has been the lead developer of the CapDL toolchain.
Michael McInerney
Senior Proof Engineer
Michael is a mathematician at heart who is applying his thorough reasoning and rigour to the art and engineering of formal proofs. He has become the main expert on the verification of MCS seL4, the configuration that supports mixed-criticality systems by providing the fundamental mechanisms to ensure timeliness.
Ryan Barry
Proof Engineer
Ryan is the author of the proofs of integrity and confidentiality for seL4’s RISC-V variant, and is specialising in interactive theorem proving and concurrency theory. He is passionate about proof engineering and believes in making formal methods as accessible as possible. Ryan is a PhD student and works for Proofcraft on a casual but crucial basis.
What is Proofcraft
-
the special skill used in creating scalable mathematical proofs.
Her theorem demonstrated impeccable proofcraft.
It takes immense proofcraft to maintain a million-line proof for over a decade.
- a vehicle for traversing proof space.
Aircraft, spacecraft, proofcraft
- the company that provides training, consulting, and proof projects with these skills.
Call the people at Proofcraft, they will tell you how to get going in software verification.
Contact Proofcraft
Want to learn more about formal methods or to set up training for your team? Interested in using formal models to enhance the assurance of your software? Want to make verified changes to seL4?
We can help.
Send us an email: contact@proofcraft.systems