Mr Matthew Brecknell

Senior Proof Engineer

Contact details:


Matthew is an experienced software engineer who has delivered software projects across a range of organisations and industries. Having felt the frustration of software failures, he became interested in using type theory and formal logic to rigorously demonstrate software fit for purpose.

In early 2016, he joined the Trustworthy Systems group at Data61 (formerly NICTA), where he works on proofs about the seL4 microkernel, using Isabelle/HOL. As a proof engineer, his biggest challenge is figuring out how to rapidly, yet sustainably, evolve a large body of proofs, to meet demand for new hardware platforms and kernel features. Current projects include verification of a version of seL4 supporting mixed-criticality real-time systems, and extending translation validation to new platforms.

Matthew also has a research group home page, and occasionally blogs about programming and formal verification.

Other Interests


Achievements and Awards

  • January 2010

    Best paper and best student paper
    Australasian Computer Science Conference

Professional Areas

Current Roles

  • Senior Proof Engineer in the Trustworthy Systems Group
    Formal software verification and related tool development

Academic Qualifications

  • 1998

    Bachelor of Engineering (Hons I - Computer Systems)
    The University of Queensland

Professional Experiences

  • July 2016-Present

    Senior Proof Engineer
    Data61 CSIRO

  • January 2016-June 2016

    Senior Proof Engineer

  • January 2014-January 2016

    Codexterity Pty Ltd

  • July 2013-September 2014

    Appsbroker Consulting Limited

  • January 2013-June 2014

    Netstorm Pty Ltd

  • 2010-2012

    Queensland University of Technology

  • 2008-2010

    Research Student
    Queensland University of Technology

  • 2004-2006

    Senior Software Engineer
    Boeing Australia

  • 2001-2004

    Senior Software Engineer
    MetaSolv Software

  • 1997-2001

    Systems and Software Engineer

  • 1996

    Software Engineer
    Octina Pty Ltd

Community and Corporate Citizenship

  • 2011-2016

    Co-organiser of the Brisbane Functional Programming Group