Logic is not universally useful in formal proofs because logic as you conceive it is incomplete. This is a provable result in the basic logic one would learn in an introductory formal methods course.

Real formalization either does not admit very obvious axioms, like excluded middle, or cannot prove theorems we would consider obvious, like function equivalence.

In formal methods in computer science and math we as of yet do not even have a complete logic that can encapsulate all the things we want to prove (homotopy type theory is an attempt but there is no accepted computational interpretation). Stop pretending 'logic' is a thing that is self evidentiary.

>logic as you conceive it is incomplete

Don't we all know that at least since Gödel.

>very obvious axioms, like excluded middle

I don't consider it something obvious. If you read Nagarjuna's Mulamadhyamaka-Karik, you might even consider it something inappropriate.

> I don't consider it something obvious.

Then that puts you in the minority of those using 'logic' when arguing about non-mathematical things. By and large, most lines of reasoning engaged in those attempting to be 'rational' rests on excluded middle.