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
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 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.
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 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.
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.
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: email@example.com