I have been trying to motivate the Frama-C people to find an excellent
intern to write a specification of the OCaml memory model in ACSL
(their specification language for C, http://frama-c.com/acsl.html );
the dream is that one may then be able to use Frama-C to check for
safety of the C stubs, and even possibly verify some parts of the C
codebase in the compiler distribution (probably not the runtime
implementation itself, which precisely breaks the abstraction of the
memory model, but at least large parts of C implementation of
primitives, otherlibs/, etc.). I think they are interested as well,
but I'm not sure they have found the time and people to work on this.