# Now It Compiles! Certified Automatic Repair of Uncompilable Protocols

## TL;DR

This paper introduces an automatic repair method for uncompilable choreographies in choreographic programming, formalizes it, and uses theorem proving to correct and validate the approach.

## Contribution

It formalizes the amendment procedure for choreographies, identifies and corrects a flaw in the original theory using theorem proving, and enhances the reliability of automatic protocol compilation.

## Key findings

- Discovered a counterexample invalidating previous theory
- Formalized amendment procedure with theorem prover validation
- Provided a corrected and verified formulation of amendment

## Abstract

Choreographic programming is a paradigm where developers write the global specification (called choreography) of a communicating system, and then a correct-by-construction distributed implementation is compiled automatically. Unfortunately, it is possible to write choreographies that cannot be compiled, because of issues related to an agreement property known as knowledge of choice. This forces programmers to reason manually about implementation details that may be orthogonal to the protocol that they are writing. Amendment is an automatic procedure for repairing uncompilable choreographies. We present a formalisation of amendment from the literature, built upon an existing formalisation of choreographic programming. However, in the process of formalising the expected properties of this procedure, we discovered a subtle counterexample that invalidates the original published and peer-reviewed pen-and-paper theory. We discuss how using a theorem prover led us to both finding the issue, and stating and proving a correct formulation of the properties of amendment.