How does TVM ensure its correctness?

My questions are:

  • Does TVM guarantee that the library of operators compiled from it will be correct?
    • If so, how is it guaranteed?
    • Is there a formal proof of that?
  • Will TVM test every release version in large quantities?
    • If so, to what extent do these tests cover?

‘correct’ means every inference process will not crash and the result is consistent with the result expected by the model