When I think about foundations I'm thinking of reducing everything to ZFC set theory + first order logic. Is this still contemporary?

The only sense in which this is contemporary is that nowadays, people are actually constructing formal proofs using computerized proof assistants, as mentioned in Andrej Bauer's answer. As Andrej mentioned, Mizar is based on set theory and first-order logic, but most proof assistants use type theory. One system not mentioned by Andrej is homotopy type theory as pioneered by Voevodsky and others. Some highly nontrivial mathematical theorems have been fully formalized, such as the Feit–Thompson theorem and the Kepler conjecture.

Another active area of research in foundations is reverse mathematics, which is concerned with examining exactly which axioms are needed for various portions of mathematics. It has long been recognized that ZFC is far stronger than necessary for formalizing most of mathematics, and so there is interest in figuring out which axioms are really needed. The standard introduction to reverse mathematics is Simpson's book, Subsystems of Second-Order Arithmetic. However, there is a lot of research into axiomatic systems not treated in Simpson's book. There are weaker systems, such as bounded arithmetic, which have close connections to computational complexity theory. In the other direction, Harvey Friedman has a long-term research program to construct natural-looking elementary combinatorial statements that cannot be proved except by assuming (the consistency of) large cardinal axioms.

Although Gödel's results tell us that we cannot expect a general decision procedure for theoremhood, there continues to be research into the decidability of various finite fragments of mathematics. As mentioned by Harvey Friedman, all three-quantifier sentences of first-order set theory are decided in a weak fragment of ZF. It is also an open problem whether Hilbert's Tenth Problem is decidable over $\mathbb Q$.

By the way, it is perhaps worth mentioning that some people equate "foundations" with "logic and set theory." I personally don't agree with this equation. There is a lot of interesting technical work in logic and set theory that I would not describe as being concerned with the foundations of mathematics as such. If you're interested in current research topics in logic, this MO question provides some information.

When I think about foundations I'm thinking of reducing everything to ZFC set theory + first order logic. Is this still contemporary?

The only sense in which this is contemporary is that nowadays, people are actually constructing formal proofs using computerized proof assistants, as mentioned in Andrej Bauer's answer. As Andrej mentioned, Mizar is based on set theory and first-order logic, but most proof assistants use type theory. One system not mentioned by Andrej is homotopy type theory as pioneered by Voevodsky and others. Some highly nontrivial mathematical theorems have been fully formalized, such as the Feit–Thompson theorem and the Kepler conjecture.

Another active area of research in foundations is reverse mathematics, which is concerned with examining exactly which axioms are needed for various portions of mathematics. It has long been recognized that ZFC is far stronger than necessary for formalizing most of mathematics, and so there is interest in figuring out which axioms are really needed. The standard introduction to reverse mathematics is Simpson's book, Subsystems of Second-Order Arithmetic. However, there is a lot of research into axiomatic systems not treated in Simpson's book. There are weaker systems, such as bounded arithmetic, which have close connections to computational complexity theory. In the other direction, Harvey Friedman has a long-term research program to construct natural-looking elementary combinatorial statements that cannot be proved except by assuming (the consistency of) large cardinal axioms.

Although Gödel's results tell us that we cannot expect a general decision procedure for theoremhood, there continues to be research into the decidability of various finite fragments of mathematics. As mentioned by Harvey Friedman, all three-quantifier sentences of first-order set theory are decided in a weak fragment of ZF. It is also an open problem whether Hilbert's Tenth Problem is decidable over $\mathbb Q$.

By the way, it is perhaps worth mentioning that some people equate "foundations" with "logic and set theory." I personally don't agree with this equation. There is a lot of interesting technical work in logic and set theory that I would not describe as being concerned with the foundations of mathematics as such. If you're interested in current research topics in logic, this MO question provides some information.