Verification of Turing-equivalent automata

Question

Correct me if I slept in my computer science studium: If an automaton is Turing-equivalent, the Halting problem shows that there are programs we can not verify (since we can't even predict their output in the first place).
Now, this is a theoretical result; in practice, software writers all over the world try to verify their programs and usually succeed. Can you give me an actual example of an automaton (Petri net, Turing machine, whatever), either...
a) one which no human understands at all, or even better (since we could cheat in "a" by simply adding complexity until our brain gives up)
b) one which is fully understood by human but nobody can prove the actual behaviour.
(It's debatable whether checkmating with King, Rook, and Bishop against King, Knight, and Knight would already constitute a valid example, since I think it falls under the complexity cheat. And maybe "b" is a contradiction in terms.)

Answer 1

(a) I think that "no human understands" what the current busiest $6$-state Busy Beaver $2$-symbol Turing Machine is doing while it prints out $3.5 \times 10^{18267}$ $1$'s before halting.

(b) This does not quite address your 2nd question as you phrased it, but there are several $5$-state quite-Busy Beavers that are believed to loop, but no one can prove they loop, or prove they halt. A list of these irregular Turing Machines is maintained here.

Incidentally, just to illustrate the complexity of Busy-Beaver questions, a $4888$-state Turing Machine has been constructed which halts if and only if there is a counterexample to Goldbach's conjecture.

Yedidia, Adam, and Scott Aaronson. "A Relatively Small Turing Machine Whose Behavior Is Independent of Set Theory." arXiv:1605.04343 (2016). (arXiv Abstract.)

Answer 2

An often-cited example of a very basic program, for which termination is open, is one that generates the Collatz sequence. In pseudo-code:

collatz(int n)
  while (n > 1)
    if (n mod 2 == 0)
      n = n / 2;
    else
      n = 3n + 1;