Model-checking (in the sense of reachability in a succinct graph) is PSPACE-complete. SAT is NP-complete. Both problems are considered intractable, yet there exist tools capable of solving them on many industrially relevant instances.
Since IP=PSPACE, I was wondering whether there are approaches capable of performing interactive proofs on "realistic" instances of co-NP-hard problems.
I am aware of Goldwasser et al.'s Delegating Computation, but they focus on tractable problems (prover in P) with a very fast verifier. I'm rather considering difficult problems, such as showing that a propositional formula is unsatisfiable.
Obviously, for model-checking, I could encode the problem into TQBF (using Savitch's construction), then use Shamir and Shen's reduction to IP. I believe, however, that this would not yet anything workable even on instances on which known model-checking algorithms (e.g. based on ROBDDs or IC3) would work. As far as I know, reducing model-checking of non-toy examples to TQBF yields formulas that none of the best QBF solvers can deal with!
I realize this is not truly a theory question, since I'm requesting an answer about "workable" solutions rather than something along the lines of "this would require a prover capable of solving intractable problems so it's impossible".