SolBehave finds compiling AI-generated Solidity often diverges from its reference

Researchers regenerated implementations for 250 verified Ethereum smart contracts and then compared each compiled candidate with its original. Their tests deliberately answer different questions: differential fuzzing searches for unexpected input behavior in function bodies, historical replay checks actual on-chain transaction sequences, and DCR-guided synthetic replay creates valid but previously unseen operation sequences. This distinction matters when access controls or balances depend on which function was called first.

The authors report compilation success of 26.4% to 92.7%, but behavioral equivalence in only 31.4% of pooled compiling regenerated function bodies. For six of seven models, 13% to 31% of compiling contracts diverged on historical replay and 13% to 44% under synthetic replay. These are reference-equivalence test results, not discovered exploits in 250 deployed contracts. The evaluated cohort is dominated by relatively small contracts, and equivalence outside tested sequences remains unproved. The public code repository contains reproduction instructions, although artifact availability wording in its README is inconsistent and an independent rerun has not been performed.

The 31.4% figure means no divergence was found by the study's differential fuzzer for that proportion of compiling function bodies; it is not a mathematical proof of equivalence. Historical replay samples what users did, whereas DCR-guided sequences explore valid states that users had not reached. The paper reports 246 to 311 additionally reached state-changing functions under different extractors, while acknowledging that the synthetic and historical oracles each miss paths the other tests.