A compositional, bottom-up verification tool that uses Large Language Models to generate natural language specifications and verify memory safety, memory leaks, and integer overflows in C/C++ functions.
Natural Language based Specification and Verification Zhaorui Li, Chengyu Song [Paper]
- Function Extraction: Uses libclang to accurately parse C/C++ source files via
compile_commands.json - Bottom-Up Analysis: Processes functions in topological order (callees before callers)
- Multiple Analysis Passes: allocation, free, init, memsafe, verify, leak, intoverflow
- LLM Integration: Supports Claude, OpenAI, Gemini, and llamacpp backends
# Clone the repository
git clone https://github.com/R-Fuzz/nlforge.git
cd nlforge
# Install with pip
pip install -e .
# For development
pip install -e ".[dev]"- Python 3.10+
- libclang (for C/C++ parsing)
- One of: Anthropic API key, OpenAI API key, Gemini API key, or local LLM
Install libclang on Ubuntu/Debian:
# Ubuntu 24.04
sudo apt-get install libclang-18-dev
# Ubuntu 22.04
sudo apt-get install libclang-14-devOn macOS:
brew install llvm# Set your API key
export ANTHROPIC_API_KEY="your-key-here"
# or
export OPENAI_API_KEY="your-key-here"
# Step 1: Extract functions from your project (requires compile_commands.json)
nlforge scan --compile-commands build/compile_commands.json --db functions.db
# Step 2: Run LLM analysis passes
nlforge summarize --db functions.db --backend claude --type allocation
# Step 3: View results and statistics
nlforge stats --db functions.db
nlforge show-issues --db functions.dbExtract functions from C/C++ source files using compile_commands.json. Must be run before summarize.
nlforge scan --compile-commands <path> [options]
Options:
--compile-commands PATH Path to compile_commands.json (required)
--db PATH Database file (default: summaries.db)
--project-path PATH Host path to project source root (for Docker path remapping)
--preprocess Run clang -E to expand macros before extraction
--verbose, -v Verbose outputGenerate summaries using LLM analysis. Requires a database populated by scan.
nlforge summarize --db <path> [options]
Options:
--db PATH Database file path (required)
--backend TYPE LLM backend: claude, openai, llamacpp, gemini (default: claude)
--model NAME Specific model to use
--type PASS Summary pass(es) to run (default: allocation). Can be specified
multiple times. Choices:
allocation – heap allocation summaries
free – deallocation summaries
init – initialization summaries
memsafe – memory safety contracts
leak – memory leak analysis (requires allocation + free)
intoverflow – integer overflow analysis
verify – full verification (requires all four prior passes)
--llm-host HOST Hostname for local LLM backends (default: localhost)
--llm-port PORT Port for local LLM backends
--disable-thinking Disable thinking/reasoning mode for llamacpp
--verbose, -v Verbose output
--force, -f Force re-summarize even if summary exists
--log-llm PATH Log all LLM prompts and responses to file
--init-stdlib Auto-populate stdlib summaries before starting
--allocator-file PATH JSON file with custom allocator names (for allocation pass)
--deallocator-file PATH JSON file with custom deallocator names (for free pass)
--vsnap PATH V-snapshot (.vsnap) file for alias context in memsafe/verify passes
-j N Parallel LLM queries (default: 1)
--cache-mode MODE Prompt caching: none, instructions, source (default: source for claude)
--function NAME Only summarize specific function(s). Can be specified multiple times.
--incremental Only re-summarize dirty functions (missing, source-changed, or callee-updated)
--exclude-unreachable-from FUNC Only process functions reachable from the given function(s)Show database statistics and call graph information.
nlforge stats [--db PATH]List verification and leak issues with review status.
nlforge show-issues --db <path> [options]
Options:
--db PATH Database file path (required)
--name TEXT Filter by function name
--status STATUS Filter by review status: pending, confirmed, false_positive, wontfix
--severity SEV Filter by severity: high, medium, low
--format TYPE Output format: table, json (default: table)export ANTHROPIC_API_KEY="your-key"
nlforge summarize --db functions.db --backend claude
nlforge summarize --db functions.db --backend claude --model claude-opus-4-5export OPENAI_API_KEY="your-key"
nlforge summarize --db functions.db --backend openai
nlforge summarize --db functions.db --backend openai --model gpt-4onlforge summarize --db functions.db --backend gemininlforge summarize --db functions.db --backend llamacpp --llm-host localhost --llm-port 8080# 1. Build your project with compile_commands.json (e.g., via cmake -DCMAKE_EXPORT_COMPILE_COMMANDS=ON)
# 2. Extract functions
nlforge scan --compile-commands build/compile_commands.json --db func-scans/myproject/functions.db -v
# 3. Run analysis passes in order
nlforge summarize --db func-scans/myproject/functions.db --backend claude --type allocation --init-stdlib
nlforge summarize --db func-scans/myproject/functions.db --backend claude --type free
nlforge summarize --db func-scans/myproject/functions.db --backend claude --type init
nlforge summarize --db func-scans/myproject/functions.db --backend claude --type memsafe
nlforge summarize --db func-scans/myproject/functions.db --backend claude --type verify
# 4. Review results
nlforge stats --db func-scans/myproject/functions.db
nlforge show-issues --db func-scans/myproject/functions.db --severity high
nlforge show-issues --db func-scans/myproject/functions.db --format json > issues.jsonIf you find NLForge useful in your research, please cite our paper:
@article{li2026nlforge,
title={Natural Language based Specification and Verification},
author={Li, Zhaorui and Song, Chengyu},
journal={arXiv preprint arXiv:2605.11315},
year={2026}
}MIT License