1. 1

  2. 1

    One thing people often get too binary on with regards to formally-verified software is whether formally-verified stuff is too impractical or math-heavy to be useful versus whether hand-coded, informal stuff is trustworthy. The actual way that an A1/EAL7 development is supposed to happen based on oldest, successful projects is for developers and verifiers to work together on a mutual understanding of each component. They each know something the others don’t about the problem. They teach each other. Each offers modifications to make the others’ job easier albeit the proof engineers are going to be asking for majority of those more due to their constraints. This write-up nicely illustrates how that works for the team behind the seL4 separation kernel (below).


    Note: Unlike most separation kernels, seL4 has an open-source version available. The other one that’s FOSS is Muen (muen.codelabs.ch) which is partially verified using SPARK Ada.