Title: Mechanical verification of concurrency control and recovery protocols