Linearizability is a key design methodology for reasoning about implementations of concurrent abstract data types in both shared memory and message passing systems. It provides the illusion that operations execute sequentially and fault-free, despite the asynchrony and faults inherent to a concurrent system, especially a distributed one. A key property of linearizability is inter-object composability: implementations of linearizable objects can be composed into more complex linearizable objects. However, devising complete linearizable objects is very difficult requiring complex algorithms to work correctly under general circumstances, and often resulting in bad average-case behavior. Concurrent algorithm designers therefore resort to speculation, namely optimizing algorithms to handle common scenarios more efficiently. Unfortunately, the outcome are even more complex protocols, for which it is no longer tractable to prove their correctness. To simplify the design of efficient yet robust linearizable protocols, we propose a new notion: speculative linarizability. This property is as general as linearizability, yet it allows intra-object composability, namely proving multiple protocol phases separately. In particular, it allows the designer to focus solely on the proof of an optimization and derive the correctness of the overall protocol from the correctness of the existing, non-optimized one. Our notion of protocol phases allows processes to independently switch from one phase to another, without requiring them to reach agreement to determine the change of a phase. To illustrate the applicability of our methodology, we show how examples of speculative algorithms for shared memory and asynchronous message passing naturally fit into our framework. We rigorously define speculative linearizability and prove our intra-object composition theorem in its trace-based as well as its mechanically checked automaton-based versions in an Isabelle I/O automata framework. This framework enables for the first time scalable specifications and mechanical proofs of speculative implementations of linearizable objects.