முக்கிய உள்ளடக்கத்திற்குத் தாவு
பாதுகாப்பு மற்றும் சோதனை

K Semantics of the Ethereum Virtual Machine (EVM)

முறைசார் சரிபார்ப்பு

GitHub இல் பார்க்க (புதிய தாவலில் திறக்கும்)X இல் K Semantics of the Ethereum Virtual Machine (EVM) (புதிய தாவலில் திறக்கும்)

அடுத்துப் பார்க்க

hax

K Semantics of the Ethereum Virtual Machine (EVM) பற்றி

KEVM என்பது EVM-இன் K-framework செயல்படுத்தக்கூடிய சொற்பொருளியல் (executable semantics) ஆகும்: உங்களுக்கு இணக்கத்தன்மை சரிபார்க்கப்பட்ட செயலாக்கம், குறியீட்டு ஆய்வு, எரிவாயு பகுப்பாய்வு அல்லது எத்திரியத்தின் விதிகளை நெருக்கமாகப் பின்பற்றும் சான்றுகள் தேவைப்படும்போது, பைட் குறியீட்டில் இதைப் பயன்படுத்துங்கள்.

குறிச்சொற்கள்

  • பாதுகாப்பு
  • கல்வி
  • பகுப்பாய்வு
  • முறைசார் சரிபார்ப்பு
  • குறியீட்டுச் செயலாக்கம்
  • பிழைத்திருத்தக் கருவிகள்
  • இயக்கநேர சரிபார்ப்பு
  • Vyper

களஞ்சியம்runtimeverification

தகவல்

வகை
முறைசார் சரிபார்ப்பு
GitHub நட்சத்திரங்கள்
595
உரிமம்
BSD-3-Clause
பட்டியல் மதிப்பாய்வு செய்யப்பட்டது
ஜூன் 2026

ஒத்த கருவிகள்

Certora Prover

Certora Prover

Certora Prover is a cloud formal-verification service that checks specifications written in CVL against deployed contract code. Verification engineers use it to prove that a contract holds stated properties for all inputs.

Kontrol - formal verification tool based on Foundry and KEVM

Kontrol - formal verification tool based on Foundry and KEVM

Kontrol ஆனது Foundry பண்புச் சோதனைகளை KEVM-ஆதரவுடைய சான்றுகளாக மாற்றுகிறது, இதனால் வெறும் KEVM-ஐ மட்டும் பயன்படுத்துவதை விட குறைவான கையால் எழுதப்பட்ட விவரக்குறிப்பு வேலைகளுடன் முறைசார் உத்தரவாதங்களை நீங்கள் பெற முடியும்.

Act

Act

Act என்பது எத்திரியத்தின் அறிவிப்பு விவரக்குறிப்பு மொழி மற்றும் கருவித்தொகுப்பாகும். இது ஒரு EVM நிரலின் அனைத்து நடத்தைகளையும் விவரிக்கப் பயன்படுகிறது, இதன் மூலம் SMT தீர்ப்பிகள், தேற்ற நிரூபிகள் அல்லது பொருளாதாரப் பகுப்பாய்வுக் கருவிகள், நடைமுறைச் செயலாக்கங்களுக்கு எதிரான தானியங்கி சுத்திகரிப்பு சான்றுகள் உட்பட, பைட் குறியீடு-நிலை சரியான தன்மை மற்றும் ஊக்கத்தொகை இணக்கத்தன்மை குறித்து பகுப்பாய்வு செய்ய முடியும்.