The cited project is about proving that a C program has no undefined behaviour. If such proof can't be found, the code may still be okay. So the existence of t

The cited project is about proving that a C program has no undefined behaviour. If such proof can't be found, the code may still be okay. So the existence of that tool doesn't contradict the statement of the article.