TLA+ для проверки корректности механизма heartbeats

Разработчики применили модельную проверку TLA+ (с использованием TLC) для верификации логики агентов в swarm-системе. Это позволило сократить пространство состояний с 1,5 млн до 4 тысяч и выявить 10 сложных ошибок, вызывавших деградацию производительности.