SPECTRA: Specification-Oriented Static Analysis for Smart Contract Security and Behavioral Contract Inference

Abstract

SPECTRA is a static-analysis framework for Solidity contracts that integrates symbolic execution, seven-domain abstract interpretation, semantic vulnerability detection, specification synthesis, SMT validation, and CEGAR refinement. Across 220 contracts, SPECTRA analyzes 216 (98.18%), infers 1,381 function-level specifications (6.39 per successful contract), and reports 673 vulnerability findings in 192 contracts (88.89%), with 0.70 s median runtime. These results indicate that specification-oriented analysis remains practical at benchmark scale.