VeriABI

This source code contains VeriABI, a formally verified tool that decides whether a new version of a C++ shared library is binary-interface compatible with its predecessor, i.e. whether it can replace the old one without recompiling dependent code. It supports the MSc thesis "Binary Interface Compatibility for Library Integration in C++" (TU Delft, 2026). The research is formal rather than empirical: a declarative specification of ABI compatibility was formalised in the Rocq (Coq) proof assistant, and a decision procedure was implemented and proven sound and complete against that specification, then extracted to OCaml and driven from a C++ front end. The deposit consists of the Rocq sources and proof scripts, the extracted OCaml code, the C++ front end, build configuration, examples and documentation, released under the Mozilla Public License 2.0.