A formal TLA+ model of a race condition in Celery's Redis broker:
when visibility_timeout expires before a worker acknowledges an ETA task,
restore_visible creates a duplicate copy, leading to double execution.
In Celery with Redis broker, each fetched task enters a "reserved" state
(invisible to other workers) for visibility_timeout seconds. If the worker