Software verifiers all report the same kinds of facts and every one of them says it differently. Anything built on top of a verifier starts by writing a parser, and that parser has to be tested, maintained, and rewritten when the tool’s output drifts. Add a second verifier and you do it again, into a second shape that doesn’t line up with the first.
formal-lib does that work once. Verifier output goes in, a stable structured
model comes out: issues with severity and error type, stack traces, and
counterexample traces with variable assignments.
Install
pip install formal-lib
Backends
ESBMC, CBMC, Clang, Kani, and PyTest are supported today.
Each backend is described by a declarative spec. Adding a verifier means adding a spec, not a parser.
Version Agnostic
Verifiers change their output between releases. Each spec declares the verifier
versions it supports, as exact versions or ranges, and formal-lib picks the
right one at parse time. When a tool changes format, a new spec is added
alongside the old one and both keep working.
This needs nothing from the verifier’s maintainers. They have no obligation to emit a format that suits downstream tools, and asking them to is the wrong place to solve the problem.
The pf CLI
pf (Pretty Format) is the command-line frontend. It runs a verifier for you:
pf -- esbmc --k-induction --k-step 2 --max-k-step 10 file.c
or reads output you already have:
esbmc --k-induction file.c 2>&1 | pf
The backend is auto-detected when you don’t name one. Output comes back as readable text or as JSON for another program to consume.
Licence
Dual licensed. Under AGPL-3.0 you can use, modify and distribute it freely, provided derivative works stay open under the same terms. For proprietary or closed-source use, a commercial licence is available from UOM Innovation Factory.