The basics of model theory contain, as far as I understand, some theorems that are difficult to prove in their full generality.
For example, the compactness theorem in FOL for languages with arbitrarily many symbols was proven by Maltsev in 1936. Gödel originally proved the countable case in 1930.
Trying to formalize model theory and make a usable library in a proof assistant seems like it would be pretty tough, since you have to make some awkward foundational choices. What exactly is $\models$? It's probably too big to be a set.
I'm wondering if there are any proof assistants out there that have a model theory library or ones that were specifically designed to tackle this area (or do other similar things, like study set-based semantics of non-classical logics with a classical set theory in the background).