Using formal methods? Yes but as an industry we simply don't know how to scale that to something as large and unwieldy as the Ruby VM.

And even if we did, correct according to what? There is no mathematical model of the Ruby language to prove it equivalent to (there are a few semantic models for Ruby but they are very limited).

And even if we had that, the computational resources needed likely are not available.