Ruka kwenda kwenye maudhui makuu

Usalama, majaribio na uthibitishaji rasmi

Zana za ukaguzi, majaribio, fuzzing, na uthibitishaji ili kuboresha usalama na usahihi wa mkataba-erevu.

Vivutio

We are Runtime Verification, a research and development company building rigorous tools to ensure the safety and correctness of critical systems. Our team has developed KEVM, the most complete and battle-tested formal semantics of the Ethereum Virtual Machine (EVM), written in the K Framework. KEVM is not just a specification, it is an executable specification that can be used to symbolically reason about smart contracts, run conformance tests, analyze gas usage, debug programs, and formally verify correctness properties. It passes the full Ethereum test suite and is used to verify high-value contracts, including ERC20 tokens in both Solidity and Vyper. We recently updated the semantics to support Pectra upgrade. KEVM is being actively utilized by Kontrol - our formal verification tool for Soldiity, which is actively used by leading teams in the EVM ecosystem, including Optimism, Ethereum Foundation, Lido, Uniswap, as well as security researchers and auditors across the broader Ethereum community. We actively maintain this repository, contribute to Ethereum’s protocol evolution, and integrate with developer tooling like Foundry. Through KEVM, we are pushing the boundaries of what’s possible in provably correct and secure smart contract infrastructure.

K Semantics of the Ethereum Virtual Machine (EVM)
Usalama, majaribio na uthibitishaji rasmi

K Semantics of the Ethereum Virtual Machine (EVM)

Usalama · Elimu · Uchanganuzi · Uthibitishaji rasmi · Utekelezaji wa kiishara · Zana za utatuzi · Uthibitishaji wa Runtime · Vyper

Matumizi

Inaonyesha (19)

Kategoria zingine za programu

Mnyororo-tofauti na utangamano

Zana zinazowezesha kutuma ujumbe, uhamisho wa mali, na hali iliyoshirikiwa kwenye mtandao mkuu wa Ethereum, unda-mpya, na minyororo mingine ya bloku.

Miundombinu ya muamala na mkoba

Miundombinu ya kujenga, kusaini, kutuma, kuiga, na kudhibiti miamala ya Ethereum na mikoba.

Data, uchanganuzi na ufuatiliaji

Zana za kuorodhesha, kuuliza, uchanganuzi, na ufuatiliaji wa data ya onchain, utekelezaji, na shughuli za mtandao.

Elimu na rasilimali za jumuiya

Nyenzo za kujifunza, nyaraka, mafunzo, na majukwaa ya jumuiya kwa wajenzi wa Ethereum.

Maktaba za wateja na SDKs (mwisho wa mbele)

Maktaba na SDKs maalum za lugha kwa ajili ya kuingiliana na nodi za Ethereum, mikataba, na itifaki.

Uendelezaji wa mkataba-erevu na mnyororo wa zana

Mifumo na zana za kuandika, kujaribu, kupeleka, na kuboresha mikataba-erevu.