Bounded automated remediation you can inspect
This demonstrator implements one explicit end-to-end mechanism: deterministic detection of an external value call followed by a state update, a bounded Checks-Effects-Interactions reorder, and re-analysis with the same rule.
1 · Solidity contract input
2 · Deterministic analyzer findings
3 · Remediation output
Automatic mechanism: reorder the precisely identified state-effect statement before the external interaction. Recommendation: additionally assess a reentrancy guard and broader behavioral tests.
4A · Before
4B · Patched
5 · Re-analysis and mitigation status
Preserved SARMF-Bench research and DOI records
This working model extends the repository while preserving its benchmark identity and citation files. Existing archival records include Zenodo 10.5281/zenodo.18754015, IEEE DataPort 10.21227/zj4q-p934, Harvard Dataverse 10.7910/DVN/0SP3OO, Mendeley Data 10.17632/kd3vcpnn9v.1, OSF 10.17605/OSF.IO/EJWDC, and the reproducibility protocol cited in the repository README.