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.