Red-black trees is a data structure of balanced binary trees. I'll show how it could be implemented and verified in MetaPRL.