More SNARK work. I don't know how I feel about this; SNARKs are as simple as SAT solving and as prone to misexplanation as monads. Still, maybe they are the way forward; after all, anything which encrypts a TM efficiently offline is going to look something like a succinct non-interactive certificate.

SNARKs have no relation to SAT solving. Also, there is no a priori reason for encrypted Turing Machine evaluation to look like a SNARK. Indeed, the operations are very different: the first involves performing computation, while the second involves checking computation