3 ms·

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

• aw1621107 2y ago
  > 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]). [0]: https://github.com/seL4/l4v https://github.com/seL4/l4v [1]: https://docs.sel4.systems/processes/style-guide.html#verification-requirements https://docs.sel4.systems/processes/style-guide.html#verific... [2]: https://trustworthy.systems/publications/nicta_full_text/7371.pdf https://trustworthy.systems/publications/nicta_full_text/737...