Охота за 16-летней ошибкой SQLite с помощью TLA+: затронут ли dqlite?

Hunting a 16-year-old SQLite WAL bug with TLA+

Мы из команды dqlite в Canonical исследуем критическую ошибку в механизме WAL базы данных SQLite, существующую с 2010 года. Используя формальную верификацию с TLA+, мы смоделировали поведение системы, чтобы понять последовательность событий, приводящих к повреждению данных, и проверить, уязвим ли наш проект dqlite к этой проблеме.

"Важным аспектом этой ошибки является не её реальное влияние, которое очень мало, а то, как долго она находилась в репозитории, как трудно было её найти и как сложно было воспроизвести."