MISRA only goes thus far.

For writing safe code in C, you should also check Frama-C and CERT Secure Coding Standards.

http://frama-c.com/

https://www.securecoding.cert.org/confluence/display/seccode...

Even better, get the algorithms written in a theorem prover which is guaranteed to generate reliable safe C code.

This is approach taken by Microsoft with P Language(Windows USB device driver stack) and F* (new TLS implementation).

Gerard Holzmann is the main author of the formal software verification tool "spin" as well as the owner of spinroot.com. I took a class on formal verification under him at Caltech.

As an anecdote, spin was used in Plan 9 to validate the kernel scheduler and the IL network protocol. It was also used to validate a very early version of the Go scheduler.

Gerard is an ACM Fellow and a member of the NAE, and has been a leader in reliable software for NASA since he came to JPL from Bell Labs.

I probably should have clicked around a bit to determine that he is the owner of that site :)