Driving a lean proof manually is a lot of effort. It's often 50x or 100x the effort of writing the initial program in the first place. The grand idea here is that if you can get a system to have a good heuristic/intuition for figuring out those proofs, you can lower this effort amplification by a lot. This makes formal verification at this level feasible for mission critical software, and also a larger slew of software we rely on.

The difficulty lies in coming up with the right formulations, and also some times altering the program to make it amenable to proof. It's quite often the case that a proof won't go through unless the program itself has the right idea.

As for the halting problem: it is highly theoretical. Lots of programs which are useful can be proven to halt for instance. Or you can just prove that the program is correct up to the point in time where the sun expansion covers the earth. There are often practical ways around such limitations, including the alteration or reformulation of the program.