My memory from the logic classes I've taken was that after Godel, mathematicians largely abandoned Hilbert's, Russell's and Whitehead's ambition of founding mathematics on logic, and largely grew disinterested in foundational issues as a whole.
As such, mathematics doesn't have a solid foundation, and most contemporary mathematicians seem to be ok with that, as long as it works and they can get interesting results.
I agree with the rest of what you wrote, but doesn't have a solid foundation seems a bit far. Mathematicians hand-wave that their proofs can be reduced to ZFC set theory and despite reasonable wariness about that hand-waving, it has so far been borne out by all efforts at deeper inspection all the way up to full machine-checked formalization.
Although I am starting to get out of my depth, my impression was that ZFC itself is (per Godel's results) inconsistent or incomplete. Here is some research to this effect:
If this is indeed the case (as it seems to my unprofessional first glance to be) then mathematics does not in fact have a solid foundation, despite its appeal to ZFC.
I'd love to hear a professional logician weigh in on this, if there are any on here.
ZFC is incomplete. There are many celebrated results that are independent of ZFC (continuum hypothesis, large cardinals (a lot aren't even known to be consistent with ZFC), Suslin's Hypothesis, etc. However, by Godel we know this is true for any reasonable foundation of mathematics (i.e. anything capable of expressing the usual version of arithmetic). So it is not something that particularly troubles either logicians or other mathematicians.
Godel's results also show that we cannot use ZFC to prove that ZFC is consistent. However, it is strongly suspected that ZFC is consistent.
In practice, very few of the results independent of ZFC affect day to day mathematical work unless you're a logician or set theorist (which honestly start to blend into each other).
Logicians are often unsatisfied with ZFC as a foundation for other reasons. These mainly amount to the clunkiness of set theory encodings. They have no notion of types so you can pose nonsense questions such as "is the number 2 a subset of the addition function?" There's no formal way of dealing with objects "larger" than sets (e.g. the collection of all sets) other than as syntactic formulas. They obscure relationships between different mathematical fields by resulting in completely different encodings for analogous structures.
This is why logicians will sometimes talk your ear off about how category theory is so much better as a foundational theory than set theory.
Again though, for the working mathematician, these flaws in ZFC as a foundation rarely matter.
I have a general algebra textbook that uses category theory as a foundation, and although I haven't gotten very far into it, my impression is that either category theory or ZFC can be used to derive the other one. As a result, it doesn't matter a whole lot where you start since you get both eventually anyway. If category theory adds tools that make it easier to prove theorems, that's great and useful, but no one really cares if it was foundational or derived.
This is one main reason why the larger mathematical community does not closely follow these foundational discussions (there are foundations that are strict extensions of ZFC but these extensions are usually conservative).
The usual response is that it would be nice if the formal foundations of mathematics corresponded more closely to the informal intuitions of mathematicians, which is arguably not true of set theoretic foundations and perhaps is more true of category theory. Whether or not you agree about the correspondence or whether even if you agree you find it at all convincing is up to you.
The short answer is "incompleteness is not a big deal" and the slightly longer answer is "if it's inconsistent, the proof of inconsistency is devilishly hard to find." If it does exist, the inconsistent part seems likely to be sufficiently esoteric that it could be "built around."
TBH, the construction of Riemann surfaces from the natural numbers is pretty well understood by the average UK undergraduate. (Natural->Integer->Rational->Real->Complex->Foundations of Reimann Surfaces). The expression of the rules of natural numbers in ZFC is fully understood by far fewer, but that’s mostly because it’s tedious.
As such, mathematics doesn't have a solid foundation, and most contemporary mathematicians seem to be ok with that, as long as it works and they can get interesting results.