Ghidra + CBMC = Assembly Model Checker philipzucker.com

Philip Zucker describes ASMC, a tool that lifts compiled assembly into CBMC’s GOTO IR using Ghidra’s p-code semantics, then checks properties such as return values, calling-convention obligations and equivalence with C code. The project supports x86-64 and RV32/64; Zucker says its lifting component is about 1,000 lines of C++ and was heavily produced with AI.