class Base {
        virtual int size() { return size_; }
    ...
    class Derived : public Base {
        virtual int size() { return rand(); }
    ...

Derived should act like a Base with slightly different implementation details. This is all LSP is. It's a fancy phrase for a very simple concept.

As I understand it, Java's Object.toString() is an example of an LSP violation because different subtypes of Object return different strings.

An LSP violation of toString() would be something that returns a string that doesn't represent the object. If you were to return the current time as a string for an object that has nothing to do with time, that would be an LSP violation.

> Subtype Requirement: Let ϕ(x) be a property provable about objects x of type T. Then ϕ(y) should be true for objects y of type S where S is a subtype of T.

Why is the exact value of the string returned not a provable property? And, to your example, if a provable property is that the returned string represents the object, how did you know it was a provable property? And how do you prove it?

The rule seems very formal, but your notions seem very informal, and I don't know how to reconcile them.

Their notions are informal, but on some level it's just the experimentalist's interpretation of LSP -- much how some physicists (loosely) argue that if you can't make measurements to prove a theory wrong then the theory doesn't matter, it might similarly be reasonable to ignore LSP with respect to properties that you don't care about (where that definition is fuzzy and hard to pin down but should represent a definitive class of things within any given single program). E.g., most people don't rely on toString() doing much more than giving a bit of human intuition into the type and properties of an object, so any implementation which respects that behavior satisfies a realist's LSP.