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