"Correctness guarantees" is a whole bucket of things you certainly have heard of, like: bounds checking, integer overflow protection, or statically safe memory allocation.

I'm not talking about a whole-program correctness proof -- although those do exist too.