There are logical systems whose formal proofs are not computer verifiable. One such example is infinitary logic in which logical statements can be infinitely long, and a specific statement in a proof may require infinitely many premises to be checked. Such logical systems have their value in studying various aspects of foundations of mathematics, but are not normally considered to properly reflect the actual human activity of proving mathematical statements.
All logical systems (first-order logic, higher-order logic, type theory, etc.) whose purpose is to capture the notion of proof as done in practice, have machine verifiable proofs. The formal property needed here is semidecidability.
Supplemental: Noah Schweber points out another example of a formal logic which is not comuputer-verifiable. Namely, we could take as the axioms of our logical system all statements that are true in a certain class of mathematical structures. Depending on what this class of structures is, we might end up with a non-computable set of axioms, which then presents a problem for verifiability. Here are some examples:
If we take ordinary Peano arithmetic and add to it as axioms all true sentences, we get a non-verifiable system by Gödel's incompleteness.
If we take all equations in the language of a group (so we can use the group unit, operation and inverses) which hold in every group, we will get a set of equations that is already generated by the standard axioms for a group theory, and therefore semidecidable (computer-verifiable).