Proofcraft, for a verified future

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 about formal verification in general or involving the seL4® microkernel specifically, you are in the right place. Send us an email at contact@proofcraft.systems

seL4 logo
Projects

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.

Training

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.

Advice

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.

Portrait of June

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.andronick@proofcraft.systems

Portrait of Gerwin

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.

gerwin.klein@proofcraft.systems

Portrait of Rafal

Rafal Kolanski

Chief Engineer

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.

rafal.kolanski@proofcraft.systems

What is Proofcraft

proofcraft /pruːfkrɑːft/:
noun
  1. 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.

  2. a vehicle for traversing proof space.

    Aircraft, spacecraft, proofcraft

  3. 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