This paper explores the use of ownership as a key auxiliary variable within Owicki-Gries framework. We explore this idea in the context of a ring buffer, developed by Amazon, which is a partial library that only provides methods for reserving (acquiring) and releasing addresses within the buffer. A client is required to implement additional functionality (including an additional shared queue) to enable full synchronisation between a writer and a reader. We verify correctness of the Amazon ring buffer (ARB) and show that the ARB satisfies both safety and progress. Our proofs are fully mechanised within the Isabelle/HOL proof assistant.