Fun2Spec

ℹ️ About

Fun2Spec is a new tool used to automatically infer code contracts for large C++ libraries.

In particular, Fun2Spec uses large language models (LLMs) to generate postcondition specifications for C++ functions.

Two case studies are presented: the Bloomberg Development Environment (BDE) library and BlazingMQ, an open source message queue solution developed at Bloomberg.

These projects contain several millions of lines of code and constitute great experiments showcasing what can be done with Fun2Spec.

We documented Fun2Spec experiments in our paper "Fun2Spec: Code Contract Synthesis At Scale", which was published at FSE 2026 in July.

:bulb: Installation

BDE Installations

To use Fun2Spec with Bloomberg's BDE codebase, the BDE CMake build system requires the following software to be preinstalled and configured on the system:

• CMake version 3.24 or later
• Ninja (recommended) or GNU Make
• Python

Clone the bde-tools and bde repositories and add bde-tools to your PATH:

 $ git clone https://github.com/bloomberg/bde-tools.git
 $ export PATH=$PWD/bde-tools/bin:$PATH      # add bde-tools to the 'PATH'
 $ git clone https://github.com/bloomberg/bde.git

Please see the complete build instructions for open source users.

Python Installation and Usage Instructions

We recommend creating a new conda/pipenv environment for installing the dependencies.

conda create -n venv_name
conda activate venv_name
conda install pip

To install all the requirements for Fun2Spec:

pip install -r requirements.txt

To run the tool with CLI, run fun2spec/main.py with the following arguments:

For example, you can run the following command to run Fun2Spec on a BDE repository given ~/bde is the local path to the clone of the repository.

python3 fun2spec/main.py --source ~/bde  --return_type pointer --count 30 --use_cache True

:page_facing_up: Results

Execution of Fun2Spec should generate a file data/results.csv. The CSV contains the following columns: