I am coincidentally researching if I could rewrite parts of a personal project in Ada (from C) to improve reliability, and so far have failed to conclude either way.
There is a blog post about rewriting a drones control system in Spark if you were curious: http://blog.adacore.com/how-to-prevent-drone-crashes-using-s...
It does exactly what you were planning. Taking C code and rewriting it in Spark in an embedded environment.
Ada/SPARK have merit if you really want to do hard real time and formal methods. That seems overkill for a personal project?
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)
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