Subtyping in object-oriented languages is widely based on Liskov’s substitution principle, which offers static correctness guarantees of type safety while abstracting implementation details. Unfortunately, the type systems of languages like Java cannot statically enforce full behavioral substitutability, and in fact there are numerous examples of libraries some of whose components are related by inheritance but not substitutable (for example, because they do not implement “optional” operations). In this paper, we present a novel approach to precisely specify and reason about substitutability in JVM languages. A distinctive feature of our approach is that it targets JVM bytecode, as opposed to a program’s source code, as it is based on the ByteBack deductive verifier. To support reasoning about substitutability, we extended ByteBack with ghost specifications, a (restricted) form of class invariants, and substitutability-preserving specification inheritance (precondition weakening and postcondition strengthening). Equipped with these features, ByteBack can now reason precisely about behavioral substitutability violations in a way that is applicable to realistic examples (such as with optional operations of Java’s List interface). Our experiments also demonstrate that ByteBack can analyze substitutability in programs written in a combination of JVM languages, including multi-language code where Scala or Kotlin code interacts with Java libraries.