Depot ha utilizado el lenguaje de especificación formal TLA+ y su model checker TLC para verificar el recolector de basura de Depot Registry v2. El equipo sostiene que los errores más difíciles en sistemas distribuidos no aparecen en una sola operación, sino en intercalados concretos: dos procesos hacen lo correcto por separado, pero en un orden no previsto, y los datos desaparecen. A escala del registro, estos casos dejan de ser teóricos y se manifiestan con frecuencia operativa.
El proceso consiste en modelar estados y transiciones, declarar invariantes y dejar que TLC explore todos los estados alcanzables. Para el GC de tres niveles, el checker recorrió 14.290.224 estados en unos 21 minutos y demostró 10 invariantes de seguridad y 2 propiedades de vivacidad. La principal invariante garantiza que un manifiesto confirmado nunca pierda el blob al que apunta. El artículo detalla también un ejemplo de carrera check-then-act en un monedero compartido para ilustrar el método.
La pieza explica por qué Depot activa el versionado de S3 en blobs inmutables y direccionados por contenido: no para conservar historial, sino como barrera de borrado, de modo que un delete elimine exactamente la versión inspeccionada y no pise un reupload concurrente. Por último, el equipo describe cómo ha dejado de escribir el modelo a mano: un agente lo genera a partir del código Go, SQL y llamadas a S3, y los ingenieros se centran en validar invariantes y abstracciones. El resultado es una especificación fiel a la implementación transacción a transacción.