Have you considered MISRA C?
Ada/SPARK have merit if you really want to do hard real time and formal methods. That seems overkill for a personal project?
Ada/SPARK have merit if you really want to do hard real time and formal methods. That seems overkill for a personal project?
Frama-C might be worth looking into if the goal is improved reliability, and they'd be able to leverage their existing C skillset.
The MISRA documentation is not very expensive and useful by itself, £15 + VAT for an ecopy: http://www.misra.org.uk/?TabId=58
It's possible to run L4 processes written in SPARK on top of seL4.
It may be easier to just generate binary code from assembly in coq (as Microsoft Research has demonstrated: http://research.microsoft.com/en-us/um/people/nick/coqasm.pd...) instead of trying to shoehorn a C compiler into a verified context and then running proofs over that for non-trivial problems.
seL4 was a huge project. Once you start reasoning about using L4 APIs, it will only become worse (eg. it's not simple to determine who has access to the pages in any L4 AddressSpace)