Next step is probably combining that with equivalent implementations in SPARK and C subset so it gets hit with about every static/dynamic analysis possible. Do it for key libraries/runtimes of these managed or interpreted languages. Result should be quite a robust TCB for the rookies or those just preferring such tools to depend on.
On unrelated note, people following Rust might like this paper where they use Rust to write a safer GC for another language:
http://users.cecs.anu.edu.au/~steveb/downloads/pdf/rust-ismm-2016.pdf
Next step is probably combining that with equivalent implementations in SPARK and C subset so it gets hit with about every static/dynamic analysis possible. Do it for key libraries/runtimes of these managed or interpreted languages. Result should be quite a robust TCB for the rookies or those just preferring such tools to depend on.