Insertion and retrieval operations in a relational database can be made more efficient using ordered indexes. The query planner decides which implementation of an ordered index to use for optimal performance. Ideally, the user should have access to a general ordered index API without being exposed to specific implementations of the index. Furthermore, each index implementation must provide consistent guarantees about the functions exposed through the API. Our main contribution in this work is a formally verified ordered index instance, which uses a B+-tree with Cursors as its underlying data structure. A secondary contribution is our approach to verifying modular, imperative C code. We accomplish these goals as follows. First, we define a general ordered index API. Then, we use the existing implementation of a B+-tree with Cursors (verified in previous work w.r.t. a B+-tree specification) to instantiate the general API and produce a B+-tree ordered index instance. Finally, we wrap up the B+-tree index instance as a Verified Software Unit. This final step allows us to make guarantees about functions exported by the module, and ensure that no unnecessary elements are exposed to the user. Our code is verified in the Coq Proof Assistant, using the tools Verified Software Toolchain (VST) and CompCert.