A formally verified ABI compatibility checker for a subset of the C++ Itanium ABI. The core compatibility rules are specified, and a checker is implemented and proven correct w.r.t. these rules in the Rocq theorem prover. It is then extracted to OCaml and linked with a C++ frontend that reads ELF/DWARF binaries.
This tool was developed as part of an internship project at ASML Netherlands B.V. in collaboration with Delft University of Technology.
./veriabi [OPTIONS] <old.so> <new.so> [consumer.ll]Options:
-S- Print symbols from both libraries-FS- Print function signatures-OS- Print object signatures-T- Print type details (structs, unions, enums)--ignore-weak- Ignore weak symbols--ignore-ns a,b- Ignore symbols from namespaces (such as boost, Qt)--include-ns a,b- Include symbols from listed namespaces--include-ref a,b- Include symbols referencing listed namespaces--check a,b- Run only specified checkers (symbols,functions,objects,types)--fuel N- Max type checking depth (default: 20)--help- Show this help message--version- Show version information
When a consumer .ll file is provided (compiled with clang -S -emit-llvm), the checker filters results to only ABI breaks relevant to that consumer.
Exit code: 0 if compatible, 1 if incompatible, 2 on execution error.
- opam (OCaml package manager)
- LLVM 19 development libraries
- libelf, libdw (elfutils, libdw-dev)
- C++17 compiler (gcc or clang)
- GTest (for tests)
Follow the official instructions, then initialise:
opam init
eval $(opam env)opam pin -n add ocaml 5.3.0
opam pin -n add rocq-core 9.1.1
opam pin -n add rocq-stdlib 9.0.0
opam install ocaml rocq-core rocq-stdlibThis installs Rocq 9.1.1 and all OCaml dependencies into the opam switch.
To step through proofs interactively in VS Code, also install:
opam install vscoq-language-serverThen install the VsRocq extension from the VS Code marketplace.
Example:
sudo pacman -S llvm19 elfutils libdw-dev gtesteval $(opam env)
./configure.sh
make -j$(nproc)This compiles the Rocq proofs, extracts the verified OCaml checker, and links everything into the veriabi executable.
make test
./consumer_test
./elf_reader_test
./dwarf_reader_test
./ir_reader_test- Missing symbols, duplicate symbols (stricter specification)
- Symbol kind changes (function to object, etc.)
- Definition removal (defined to undefined)
- Binding strength changes (weak/strong)
- RTTI typeinfo removal
- Return type mismatches
- Parameter type mismatches
- Parameter count changes
- Variadic flag changes
- Global variable type changes
- Struct/union size and alignment changes
- Member type changes (matched by byte offset)
- Member removal
- Bitfield layout changes (slot repacking, size, type)
- Base class addition, removal, offset changes
- Virtual inheritance changes
- VTable slot reordering, removal, and content changes
- Enum size and value changes (when the enum type is used in exported signatures)
When provided with an LLVM IR file of the consumer binary, the checker narrows the report to only breaks that affect that specific consumer, based on:
- Which symbols the consumer references
- Which vtable slots the consumer calls
- Which struct members the consumer accesses
- Which types the consumer stack-allocates
- SONAME change detection
- Full vtable reconstruction from class hierarchy (to cover inherited but not overridden slots)
- Inter-procedural consumer analysis (track vtable accesses through wrapper functions)
- GCC support for consumer analysis (currently requires clang for LLVM IR), maybe binary lifting?
- Bitfield diagnostics (when the compiler shifts later bitfields into freed bits, infer likely renames/removals instead of reporting raw slot mismatches)
- Warn the user if fuel runs out when the checker is running
- Fix symmetry issue when encountering
const foo::bar *in the parser, causing aMemberTypeMismatchfalse positive