A Python library that provides structured representations of software verifier output.
- PyPI (Recommended)
- GitHub Releases
The following backends are supported:
- ESBMC
- CBMC
- Clang
- PyTest
- Kani
Each backend is parsed by a spec that declares which verifier versions it supports, as exact versions and/or inclusive version ranges (a missing bound means the range is unbounded on that side; the default is all versions). When a verifier changes its output format, a new spec is added for the new versions alongside the old one. Within a backend, no two specs may support the same version (a spec conflict). Check this with:
hatch run check-specs # fails on any spec conflict
hatch run check-specs -v # also lists every spec and the versions it supportspf (Pretty Format) is a CLI frontend for formal-lib. It can be invoked from
the CLI to get formatted output from any supported backends. There are two ways
to invoke pf; detailed below.
The verifier command is specified after the -- separator. Any builtin backend
can be specified. For example:
pf -- esbmc --k-induction --k-step 2 --max-k-step 10 file.cThis makes it easier for some backends that use stderr like ESBMC as you don't
need to redirect stderr to stdout before piping.
Pipe verifier output to pf to parse it into structured output:
esbmc --k-induction --k-step 2 --max-k-step 10 file.c 2>&1 | pfPiping as a method of invocation cannot measure the duration of execution, so that detail will be omitted from the output.
The following section shows some simple examples of the capability of
formal-lib.
from pathlib import Path
from formal_lib import VerifierRunner
verifier = VerifierRunner(base_cmd=Path("/usr/bin/esbmc"), default_timeout=120)
result = verifier.verify_source(Path("main.c"))
for issue in result.issues:
print(f"[{issue.severity}] {issue.error_type}: {issue.message}")from formal_lib import detect_spec, IssueSpecOutputParser
output = open("verifier.log").read()
spec = detect_spec(output)
parser = IssueSpecOutputParser(spec)
result = parser.parse_output(output=output)
# Drop traces from system headers or other files not in your project
project_files = {Path("main.c"), Path("lib/utils.c")}
result = result.filter_traces(project_files)
for issue in result.issues:
print(f"[{issue.severity}] {issue.error_type}: {issue.message}")from pathlib import Path
import litellm
from formal_lib import VerifierRunner
from formal_lib.specs import esbmc_spec
from formal_lib.issue import VerifierIssue
verifier = VerifierRunner(base_cmd=Path("/usr/bin/esbmc"), regex_spec=esbmc_spec)
result = verifier.verify_source(Path("main.c"))
if not result.successful:
issue = result.primary_issue
counterexample = ""
if isinstance(issue, VerifierIssue):
counterexample = f"\nCounterexample:\n{issue.counterexample_formatted}"
source = Path("main.c").read_text()
response = litellm.completion(
model="gpt-4o",
messages=[
{
"role": "user",
"content": (
f"Fix the following {issue.error_type} in {issue.file_path}:{issue.line_number}:\n"
f"{issue.message}\n\n"
f"Stack trace:\n{issue.stack_trace_formatted}"
f"{counterexample}\n\n"
f"Source:\n```c\n{source}\n```"
),
}
],
)
print(response.choices[0].message.content)If you use formal-lib in your work, please cite it using the following BibTeX entry:
@misc{charalambous2026formallib,
author = {Charalambous, Yiannis},
title = {formal-lib: A shared interface for software verifier output},
year = {2026},
howpublished = {\url{https://github.com/ByteRepair/formal-lib}},
}Please cite the version you used; see the Releases page.
Copyright © 2026 The University of Manchester. Authored by Yiannis Charalambous.
[!NOTE] This project is offered under a dual-licence model: the open-source GNU AGPL-3.0, or a separate commercial licence for proprietary use.
For a commercial licence, contact UOM Innovation Factory (the commercialisation subsidiary of The University of Manchester) at contact@uominnovationfactory.com.