That runtime system is huge. I remember it was an obstacle to high-assurance in Haskell. Is there a detailed write-up on what those 80,000loc do? Maybe someone could redo it in one of the verifying, imperative languages like SPARK or ATS to increase its assurance without full verification.