Challenge one from the VerifyThis2018 competition: specifying and verifying the behaviour of a gap buffer; a data-structure commonly used in text editors. In particular, we verify the correctness of four standard operations on gap buffers, for moving the text cursor (functions 'left' and 'right'); for inserting a character at the cursors' position (function 'insert'); and for deleting the character at the cursors' position (function 'delete'). Our general approach to show functional correctness is to represent the buffer’s content as a sequence of integers. We prove that, after executing one of the four functions, the contents of the buffer is still validly represented by the proper integer sequence.