I don't know anything about formal correctness proofs but my imagination tells me it is bounded by the description of the task. Aren't we just shifting the bugs toward the task description? Or is it about being able to specify a task with a very simple program (e.g. brute force) that is unfeasible to run but can be somehow used to verify that simpler (in terms of runtime complexity) programs provide the same outputs?

Yes. Figuring out what a program SHOULD do is often as hard as figuring out how to actually do it. The relative difficulty shifts depending how far you are from the real world. The closer your project is to actual people doing actual work, the harder it is to define the requirements precisely.

Yes, they can only logically deduce correctness based on our assumptions of a given system boundary. But I think it is typically a good idea to write them down formally if you need the guarantees. They are also typically smaller and more declarative.

Sure, if your task description/specification is buggy nothing can save you, but if you only have to check the spec your work gets much easier. If you write a program, you have to both make sure that the spec is correct and that the spec is correctly implemented.

Very good question! Try to figure it out yourself and you will see what is wrong with software development today.