# bytecode-level formal verification tools detect compiler-introduced vulnerabilities that source-level analysis cannot reach Most security tools operate at the source level, implicitly trusting that the compiler faithfully translates source semantics into bytecode. Bytecode-level tools make no such assumption, analyzing compiled output directly. KEVM provides complete formal EVM semantics, enabling verification at the execution layer below the compiler. Since [[compiler bugs represent a distinct threat category where source-level security analysis is structurally insufficient]], and since [[the Curve Finance Vyper compiler exploit proved that source-level reentrancy guards can be silently broken by compiler bugs invisible to auditors]], the financial consequences of trusting compiler output are measurable in hundreds of millions. Source-level analysis of the Vyper contracts that lost $50-70M in July 2023 would have shown correct `@nonreentrant` decorators; only bytecode inspection would have revealed the broken lock. Bytecode-level tools introduce complexity: compiler optimizations, dynamic loading, and information lost during compilation complicate verification and diagnostics. The trade-off is genuine but necessary for defense-in-depth when the compiler itself is a trust boundary. Since [[combining multiple security analysis tools detects more unique vulnerabilities than any single tool because each tool has distinct blind spots and corpus management strategies]], bytecode-level tools cover a blind spot source-level tools structurally cannot address. --- Relevant Notes: - [[compiler bugs represent a distinct threat category where source-level security analysis is structurally insufficient]]: foundation: the threat class this tool approach is designed to address - [[the Curve Finance Vyper compiler exploit proved that source-level reentrancy guards can be silently broken by compiler bugs invisible to auditors]]: example: the canonical exploit where bytecode-level verification would have detected the bug that source-level analysis missed - [[KEVM provides complete executable formal semantics of the EVM enabling correct-by-construction verification but requires deep K-framework expertise that limits practitioner adoption]]: extends: details the EVM-semantics approach to bytecode-level verification - [[formal verification can only prove properties that are explicitly specified leaving unspecified behaviors outside its guarantee boundary]]: extends: bytecode-level verification still faces the specification completeness problem - [[combining multiple security analysis tools detects more unique vulnerabilities than any single tool because each tool has distinct blind spots and corpus management strategies]]: extends: bytecode-level tools cover a distinct blind spot that source-level tools cannot address - [[whether systematic notification mechanisms exist for compiler bug disclosure to deployed protocols when bugs are fixed without security advisories]]: extends: bytecode analysis of deployed contracts is a prerequisite for any systematic notification pipeline; inventorying affected contracts requires reading deployed bytecode at scale Topics: - [[vulnerability-patterns]] - [[security-patterns]]