What kinds of systems are available that accept a certain program $P$ and attempts to figure out "the program does terminate" or "the program does not terminate" and output a proof of one or the other?
Yes, an example of a system that performs this task is T2. It does not solve the halting problem but instead it only attempts to solve certain special cases. A overview is at https://en.wikipedia.org/wiki/Microsoft_Terminator . The newest version of this system is at https://mmjb.github.io/T2/ .