Is there any second-order logic finite satisfiability checker?
There are Nitpick and Nunchaku that are model finders for higher-order logic.
Nunchaku is more recent and can build models for axioms containing higher-order quantification. But, as the problem is generally undecidable, it may not find a (finite) model even if one exists.