This is a bit beyond what you are seeking, but nevertheless
you might be interested in the work of Adam Yedidia and Scott Aaronson. They have constructed three different Turing machines, $G$, $R$, and $Z$, that have these properties:

$G$: Halts iff Goldbach's conjecture is false.

$R$: Halts iff the Riemann hypothesis is false.

$Z$: Cannot be proved in ZFC to not halt. If it halts, it proves ZFC is inconsistent. "$Z$ is a Turing machine for which the question of its behavior (whether or not
it halts when run indefinitely) is equivalent to the consistency of ZFC."

Their work is intricately related to the Busy Beaver function,
and certainly involves "state-of-the-art program analysis."

"A Relatively Small Turing Machine Whose Behavior Is Independent of Set Theory."
arXiv:1605.04343. 2016.

"The 8000th Busy Beaver number eludes ZF set theory: new paper by Adam Yedidia and me."
Scott Aaronson blog

Their appendix contains a precise description of the $7,918$-state TM $Z$, a snippet of which looks like this:

To attempt respond to the original intent of your question more directly,

"which strings of consecutive symbols on the tape are possible or impossible, and so on"

You probably know that:

(1) Finding a TM that accepts (say) all strings of exactly
length $3$ is undecidable. This can be established via Rice's theorem.

(2) Detecting "dead code," i.e., unreachable states of a TM, is undecidable.

(3) Deciding whether a TM accepts any word at all, is undecidable.