Formal Verification, часть 7.2
про _safeTransfer()

Что я имею в виду. Полный стек вызова выглядит так:

Staking._stake()
    │
    ▼
SafeERC20.safeTransferFrom()  ← CVL summary перехватывает ЗДЕСЬ
    │                            
    ✗                            
SafeERC20._safeTransferFrom() ← никогда не достигается
    ✗
assembly call                  ← никогда не достигается
    ✗
Token.transferFrom()           ← никогда не достигается

4. Решением стало проводить суммаризацию на уровне SafeERC20.safeTransferFrom(), до появления assembly блока, что позволило корректно менять состояние ghost переменной

Как обычно, теперь, оглядываясь назад, кажется, что это достаточно очевидные вещи, но это конечно не так, учитывая сколько времени я потратил на то, чтобы во всем этом разобраться. Естественно, что для погружения в эти дебри я использовал всю известную мне мощь нейронок, включая NotebookLM и Claude, это сильно помогло, но еще раз доказало насколько тяжело языковым моделям в новых областях знаний

https://t.me/web3securityresearch