Мы — Runtime Verification, научно-исследовательская компания, создающая строгие инструменты для обеспечения безопасности и корректности критически важных систем. Наша команда разработала KEVM, наиболее полную и проверенную в боях формальную семантику виртуальной машины Ethereum (EVM), написанную на K Framework. KEVM — это не просто спецификация, это исполняемая спецификация, которую можно использовать для символьного рассуждения о смарт-контрактах, запуска тестов на соответствие, анализа использования газа, отладки программ и формальной проверки свойств корректности. Она проходит полный набор тестов Ethereum и используется для проверки ценных контрактах, включая токены ERC-20 как на Solidity, так и на Vyper. Недавно мы обновили семантику для поддержки обновления Pectra. KEVM активно используется Kontrol — нашим инструментом формальной верификации для Solidity, который активно применяется ведущими командами в экосистеме EVM, включая Optimism, Ethereum Foundation, Lido, Uniswap, а также исследователями безопасности и аудиторами в более широком сообществе Ethereum. Мы активно поддерживаем этот репозиторий, вносим вклад в эволюцию протокола Ethereum и интегрируемся с инструментами разработчиков, такими как Foundry. С помощью KEVM мы расширяем границы возможного в доказуемо корректной и безопасной инфраструктуре смарт-контрактов.
