amk: Гарантий нет. Более того, уже доказано, что невозможно составить алгоритм, который получив на вход произвольную программу, выдаст гарантированное заключение об её корректности.
Обязательно среди всех возможных программ найдётся некоторое количество, которые этим алгоритмом проверить не удастся. И хорошо, если алгоритм об этой неудаче сообщит.

https://forum.sources.ru/index.php?showtopic=421132&view=findpost&p=3848036