Byzantine-fault-tolerant (BFT) protocols allow distributed systems to function correctly even when some of the nodes act maliciously. Byzantine linearizability, as an extension of linearizability in the presence of faulty nodes, is often used as the correctness criterion for BFT protocols. In this paper, we propose a program logic for verifying Byzantine linearizability. We reason about the effects of faulty nodes using a helping mechanism that instruments the protocol code with abstract operations that model the faulty nodes’ behaviors in the views of correct nodes. We prove the soundness of our logic by establishing a contextual refinement that is equivalent to Byzantine linearizability. We apply our logic to verify two typical BFT protocols.