Jesteśmy Runtime Verification, firmą badawczo-rozwojową tworzącą rygorystyczne narzędzia zapewniające bezpieczeństwo i poprawność systemów krytycznych. Nasz zespół opracował KEVM, najbardziej kompletną i sprawdzoną w boju formalną semantykę Maszyny Wirtualnej Ethereum (EVM), napisaną w K Framework. KEVM to nie tylko specyfikacja, to wykonywalna specyfikacja, która może być używana do symbolicznego wnioskowania o inteligentnych kontraktach, uruchamiania testów zgodności, analizowania zużycia gazu, debugowania programów i formalnej weryfikacji właściwości poprawności. Przechodzi pełny zestaw testów Ethereum i jest używana do weryfikacji kontraktów o wysokiej wartości, w tym tokenów ERC-20 zarówno w Solidity, jak i Vyper. Niedawno zaktualizowaliśmy semantykę, aby obsługiwała aktualizację Pectra. KEVM jest aktywnie wykorzystywany przez Kontrol - nasze narzędzie do formalnej weryfikacji dla Solidity, które jest aktywnie używane przez wiodące zespoły w ekosystemie EVM, w tym Optimism, Ethereum Foundation, Lido, Uniswap, a także badaczy bezpieczeństwa i audytorów w szerszej społeczności Ethereum. Aktywnie utrzymujemy to repozytorium, przyczyniamy się do ewolucji protokołu Ethereum i integrujemy się z narzędziami deweloperskimi, takimi jak Foundry. Poprzez KEVM przesuwamy granice tego, co jest możliwe w dającej się udowodnić, poprawnej i bezpiecznej infrastrukturze inteligentnych kontraktów.
