[dfabulich]

The last line of the abstract has the most important takeaway.

> As a consequence of this succinctness, we show that basic verification problems for transformers, such as emptiness and equivalence, are provably intractable: specifically, EXPSPACE-complete.

If you were hoping to formally prove the correctness of a large transformer, it turns out that you're going to need an exponentially larger amount of space to do your verification, more than you could possibly afford.

[ebiederm]

How does it follow that there is no point in trying for formal correctness? In many problems there is an interesting subset that is quickly solvable even when the general case is not.

SAT solvers in practice are quick on just about everything.

SAT solvers being programs that solve the original NP-compete problem.