Jsme Runtime Verification, výzkumná a vývojová společnost budující rigorózní nástroje k zajištění bezpečnosti a správnosti kritických systémů. Náš tým vyvinul KEVM, nejkompletnější a praxí prověřenou formální sémantiku pro Ethereum Virtual Machine (EVM), napsanou v K Framework. KEVM není jen specifikace, je to spustitelná specifikace, kterou lze použít k symbolickému uvažování o chytrých kontraktech, spouštění testů shody, analýze spotřeby plynu (gas), ladění programů a formálnímu ověřování vlastností správnosti. Prochází celou testovací sadou Etherea a používá se k ověřování kontraktů s vysokou hodnotou, včetně tokenů ERC-20 v Solidity i Vyperu. Nedávno jsme aktualizovali sémantiku, aby podporovala aktualizaci Pectra. KEVM aktivně využívá Kontrol – náš nástroj pro formální verifikaci pro Solidity, který aktivně používají přední týmy v ekosystému EVM, včetně Optimism, Ethereum Foundation, Lido, Uniswap, a také bezpečnostní výzkumníci a auditoři napříč širší komunitou Etherea. Tento repozitář aktivně udržujeme, přispíváme k vývoji protokolu Etherea a integrujeme se s vývojářskými nástroji, jako je Foundry. Prostřednictvím KEVM posouváme hranice toho, co je možné v prokazatelně správné a bezpečné infrastruktuře chytrých kontraktů.
