I'm curious about the c with sel4-style checking that was mentioned. Does sel4 have a style checker and/or proof checker that you can run on your c code? Or do they just have some style guide you have to read and memorize?
> Does sel4 have a style checker and/or proof checker that you can run on your c code?
The specification and proofs are open-source [0], but I suspect that they are tailored for seL4-related uses and probably aren't well-suited for "general-purpose" C code. I think using their proofs would also necessitate writing a specification for your own code which is probably going to be an ordeal in and of itself.
They do have a style guide [1] as well, but that's just a small part of the full verification process (described in [2]).
The specification and proofs are open-source [0], but I suspect that they are tailored for seL4-related uses and probably aren't well-suited for "general-purpose" C code. I think using their proofs would also necessitate writing a specification for your own code which is probably going to be an ordeal in and of itself.
They do have a style guide [1] as well, but that's just a small part of the full verification process (described in [2]).
[0]: https://github.com/seL4/l4v
[1]: https://docs.sel4.systems/processes/style-guide.html#verific...
[2]: https://trustworthy.systems/publications/nicta_full_text/737...