The cryptographic techniques and bytecode analysis powering Sigvex's multi-runtime decompiler.
Vulnerability Detection via Equality Saturation
How the CST engine uses e-graphs and equality saturation to detect EVM vulnerability patterns in under a second, without external solver dependencies.
Dynamic Vulnerability Discovery for Smart Contracts
How coverage-guided fuzzing, concolic execution, and domain-specific mutation strategies find vulnerabilities that static analysis misses and generate proof-of-concept exploits.
Beyond Opcode Translation
How Sigvex reconstructs high-level semantics from raw bytecode, recovering types, structures, and patterns that compilation erased—and why this foundation is essential for accurate vulnerability detection.
Learning from Historical DeFi Exploits
An analysis of recurring vulnerability patterns extracted from real-world smart contract exploits, and how those patterns inform automated detection.
Severity × confidence: turning 130+ detectors into a triage order
Why a detector count is not a capability. The contribution of the EVM detection framework is a two-axis model — severity and calibrated confidence, both grounded in bytecode — that tells an auditor what to open first.
EVM Bytecode to Readable Solidity
A technical walkthrough of the multi-stage EVM decompilation pipeline: how raw bytecode is parsed, lifted through two intermediate representations, and emitted as readable Solidity or Yul.
Bytecode-Native Analysis Across EVM and SVM Runtimes
An architectural overview of the Sigvex analysis pipeline: bytecode-native design, over 300 detectors spanning EVM, SVM, and ZK runtimes, and e-graph constraint satisfaction for security analysis without verified source code.
Security Analysis for eBPF Bytecode at Scale
How Sigvex analyzes Solana programs at the bytecode level, from ELF parsing and eBPF disassembly through HIR lifting, CPI analysis, and over 170 Solana-native vulnerability detectors.
Call Graphs and Inter-Procedural Security
How Sigvex constructs inter-contract call graphs and performs cross-boundary taint analysis to detect vulnerabilities that span multiple smart contracts—catching attack patterns that single-contract analysis fundamentally cannot see.
From Detection to Proof-of-Concept in Minutes
How the exploit generator synthesizes executable proof-of-concept transactions from vulnerability findings—covering reentrancy, integer arithmetic, access control, oracle manipulation, and delegatecall hijacking.
Blue Team Strategies for Smart Contract Security
Defense-in-depth strategies for smart contract security using static analysis, runtime monitoring, and automated threat detection.
A Formal Model of Smart Contract Reentrancy Through Concurrency Theory
Formal treatment of smart contract reentrancy as unsafe interleaving of execution frames, connecting detection to serializability analysis from concurrency theory.
Information Flow Analysis for EVM and eBPF Bytecode
Lattice-based taint analysis framework for stack-based virtual machines, with formal transfer functions and precision analysis for smart contract security.
Opaque Predicates, Decidability Limits, and Practical Workarounds
Analysis of how cryptographic hash functions create fundamental limits for symbolic execution in smart contract analysis, with strategies for practical soundness.
Detecting Under-Constrained Circuits and Prover-Forgeable Witnesses
Formal analysis of zero-knowledge circuit soundness, with detection algorithms for under-constrained signals and prover-forgeable witness vulnerabilities.
Hindley-Milner-Style Type Recovery for EVM Bytecode
Formal framework for recovering Solidity storage layouts from EVM bytecode using constraint-based type inference, with extensions for packed storage and proxy patterns.
Automated Exploit Construction as Syntax-Guided Synthesis
Formal framework for automated exploit generation using syntax-guided program synthesis, with finding-guided search pruning and fork-based correctness oracles.
Share inflation and rounding direction without source
How to detect ERC-4626 share-inflation and rounding-direction vulnerabilities from compiled contracts, where the defining evidence is not what the arithmetic computes but which way it rounds.
Red Team Methodology for Smart Contract Vulnerability Research
Systematic techniques for discovering new smart contract vulnerability classes through bytecode analysis, fuzzing, and exploit synthesis.
Why a detector should never type a float by hand
Replacing hand-typed confidence values with a small ladder of named evidence classes, what the migration turned up in the detectors, and why the number a detector emits is load-bearing long after anyone reads it.
Recognising guards structurally in stripped EVM bytecode
A family of detector predicates keyed on operand names was inert on every real contract, and because those predicates suppress findings, inert meant fail-open. This is how we measured it, what replaced each name test, and why the obvious structural replacement is usually worse.
When a claim about Solana bytecode cannot be grounded
Two Solana detectors were removed this month, not because they were wrong about the vulnerability but because the fact they needed to observe does not exist in compiled programs. This is the census that found them, the measurements that settled each case, and the one detector that was nearly retired and instead went from 44 findings to one.
Provenance from panic locations in stripped Solana binaries
Detectors need to know which functions in a deployed program are the author's and which are SDK. On stripped mainnet binaries the old answer attributed 96 to 99.6 percent of every program to the SDK. The fix reads a record rustc leaves behind at every panic site, and it only ever withholds a demotion.
Test metrics for a decompiler that cannot be argued with
A decompiler's test suite is mostly measurements, and a measurement that cannot fail is decoration. Five rules we now hold every metric to, each learned from a metric that had quietly stopped measuring anything.
Parser, graph model and threshold bugs in ZK circuit analysis
None of the defects fixed in the ZK analyser this month were in constraint logic. One was a comma, one was a name shared by a component port and a local signal, and one was a confidence score that depended on which compiler pipeline built the verifier. Each made a soundness verdict wrong in a way the constraint reasoning could not see.
Experience the power of these innovations on your own smart contracts.
Analyze a Contract