For the JS lifetime machinery that's entirely out of rust's borrow checker shouldn't one verify the properties of unsafe code (which I imagine the garbage colle

For the JS lifetime machinery that's entirely out of rust's borrow checker shouldn't one verify the properties of unsafe code (which I imagine the garbage collector would use)? As I understand it, Rusthornbelt exists to prove unsafe code at the cost of manual verification. As someone who's a novice in verification using model checkers, writing proofs for simple algorithms is hard enough already, so I don't see the viability of a fully verified JIT. Is there a CompCert-C equivalent for V8/JSC?