Vector Clocks in Coq: An Experience Report

TL;DR

This paper details the implementation of vector clocks within the Coq proof assistant and their integration into a production Erlang system, highlighting technical challenges faced during extraction and deployment.

Contribution

It presents the first experience of extracting verified vector clocks from Coq for use in a real-world distributed data store, addressing practical integration issues.

Findings

Successful extraction of vector clocks from Coq to Erlang

Identification of key challenges in integrating proof assistant code into production systems

Insights into the practical use of formal verification in distributed systems

Abstract

This report documents the process of implementing vector clocks in the Coq proof assistant for extraction and use in the distributed Dynamo-inspired data store, Riak. In this report, we focus on the technical challenges of using Core Erlang code extracted from the proof assistant in a production-grade Erlang application, as opposed to verification of the model itself.