Provably Correct Runtime Monitoring