저희는 중요한 시스템의 안전성과 정확성을 보장하기 위한 엄격한 도구를 구축하는 연구 개발 회사인 Runtime Verification입니다. 저희 팀은 K 프레임워크로 작성된 이더리움 가상 머신(EVM)의 가장 완벽하고 실전 테스트를 거친 공식 시맨틱인 KEVM을 개발했습니다. KEVM은 단순한 사양이 아니라 스마트 컨트랙트를 심볼릭하게 추론하고, 적합성 테스트를 실행하고, 가스 사용량을 분석하고, 프로그램을 디버깅하고, 정확성 속성을 공식적으로 검증하는 데 사용할 수 있는 실행 가능한 사양입니다. 전체 이더리움 테스트 스위트를 통과하며 Solidity 및 Vyper의 ERC-20 토큰을 포함한 고가치 컨트랙트를 검증하는 데 사용됩니다. 최근에는 Pectra 업그레이드를 지원하도록 시맨틱을 업데이트했습니다. KEVM은 Optimism, 이더리움 재단, Lido, Uniswap을 포함한 EVM 생태계의 선도적인 팀뿐만 아니라 광범위한 이더리움 커뮤니티의 보안 연구원 및 감사자가 적극적으로 사용하는 Solidity용 공식 검증 도구인 Kontrol에서 활발히 활용되고 있습니다. 저희는 이 리포지토리를 적극적으로 유지 관리하고, 이더리움의 프로토콜 발전에 기여하며, Foundry와 같은 개발자 도구와 통합합니다. KEVM을 통해 저희는 증명 가능할 정도로 정확하고 안전한 스마트 컨트랙트 인프라에서 가능한 것의 경계를 넓히고 있습니다.
