# Must all models of ZFC (in a standard formulation) be at least countable?

Must all models of ZFC (in a standard formulation) be at least countable?

Why I think this: there are countably many instances of Replacement, and so, if a model is to satisfy Replacement, it must have at least countably many satisfactions of it.

Does my question only apply to first-order formulations of ZFC, or are there second-order formulations of ZFC that can be finite?

Thanks.