&gt;That&#x27;s correct in theory, but in practice I&#x27;d be very surprised to see a useful program that couldn&#x27;t be verified by ZFC.<p>I think you do too much easy theory if you think that, if you&#x27;ll excuse my saying so.  A lot of the firmware code I write at work is just not going to be formally verifiable in any practical way without scrapping it and rewriting in a language built around formal verification from day one.<p>Besides which, a Python interpreter is a very common sort of program to write, actually, and I don&#x27;t expect that you can &quot;just&quot; do the equivalent of `Require Import ZFC` to verify its behavior properly.