formal-lib

A Python library that provides structured representations of software verifier output.

Installation

• PyPI (Recommended)
• GitHub Releases

Backends

The following backends are supported:

• ESBMC
• CBMC
• Clang
• PyTest
• Kani

Spec Versioning

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 supports

Frontend

pf (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.

Using the -- Separator (Recommeded)

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.c

This makes it easier for some backends that use stderr like ESBMC as you don't need to redirect stderr to stdout before piping.

Pipe

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 | pf

Piping as a method of invocation cannot measure the duration of execution, so that detail will be omitted from the output.

Library Examples

The following section shows some simple examples of the capability of formal-lib.

Running a Verifier

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}")

Analyzing Verifier Output

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}")

Passing ESBMC output to LiteLLM

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)

Cite

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.

License

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.