Are there logical systems where formal proofs are not computer verifiable?
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).
If you take "proof" as a convincing argument (to error probability smaller than arbitrary epsilon) that a proposition is true, then two other possibilities come to mind:
Probabilistically checkable proofs, where you have a conventional first-order proof (like your secret unpublished proof of RH) and you can convince me through a cryptographic-like protocol that you really do have a proof, without revealing how the proof works. Zero-knowledge proofs are related to this; and
(Due to L. Levin) if you believe there are physically realizable ways of generating algorithmically random numbers (e.g. by rolling dice), you can make almost-certainly-true but unprovable statements, like that the string produced by 1000 bits of coin flips can't be compressed to less than half its original length (this is an assertion about the Kolmogorov complexity, which is uncomputable).
It follows from the second example above that the physics assertion that you can generate random numbers through quantum processes is scientifically unverifiable, if you believe the Church-Turing thesis.
There are, of course, various constructivist and intuitionistic foundational theories which take the notion of an absolute, intuitive notion of proof as the basic primitive notion. It is well known that it cannot coincide with any mechanically checkable notion of proof (if one sticks to any standard intuitionistic logic, then the totality of axioms cannot be decidable). It is, though, debatable just how rigorous this then is.