We will soon have ScAfee but for Dapps!
Is it not true that program synthesis will work, as long as a "contract" isn't too large or designed adversarially? Because if that weren't true you'd have a debugger for all circuits and programs (suitably restricted in computing power).