verify-cbl

Neuro-Symbolic Formal Verification Engine for COBOL to Java Migration

---

Demo Video

---

Abstract

verify-cbl detects penny drift (rounding discrepancies) between COBOL and Java financial calculations using the Z3 SMT solver with Monte Carlo fuzzing fallback. A self-correcting LLM agent translates COBOL to mathematically proven Java BigDecimal code.

Problem Statement: Standard LLM translation produces semantically incorrect Java code due to differences in rounding semantics (COBOL ROUNDED uses HALF_UP; Java double truncates). This causes cumulative financial drift at scale.

Solution: Formal verification via satisfiability modulo theories (SMT) with automatic counter-example generation and LLM self-correction loop.

---

Table of Contents

• System Architecture
• Quick Start
• Installation
• CLI Reference
• Python API
• Verification Pipeline
• Supported COBOL Features
• LLM Providers
• Testing
• Benchmarks
• Docker Deployment
• License

---

System Architecture

flowchart LR
    A[COBOL Source] --> B[Parser]
    B --> C[IR Expression Tree]
    C --> D[LLM Translation]
    D --> E[Java BigDecimal]
    E --> F{Z3 Solver}
    F -->|equivalent| G[✓ Verified Output]
    F -->|drift| H[Error Diagnosis]
    H --> D
    F -->|timeout| I[Fuzzing 100k]
    I --> G

Loading

Pipeline: COBOL → IR → LLM → Java → Z3 verification → Output (with self-correction loop on errors)

---

Quick Start

# Install
uv pip install -e ".[all]"

# Verify single statement
verify-cbl check \
  --cobol "COMPUTE WS-TAX ROUNDED = WS-AMOUNT * 0.22." \
  --cobol-vars "WS-AMOUNT:9(7)V99,WS-TAX:9(6)V99" \
  --java "double tax = amount * 0.22;"

# Translate COBOL file
verify-cbl translate -s payroll.cbl -o Payroll.java --llm ollama

# Run Streamlit demo
uv run streamlit run demo/streamlit_app.py

---

Installation

Prerequisites

Requirement	Version	Purpose
Python	3.12+	Runtime
uv	latest	Package manager (recommended)
Ollama	optional	Local LLM inference

Install Options

git clone https://github.com/yourusername/verify-cbl.git
cd verify-cbl

# Core (Z3 verification, CLI)
uv pip install -e .

# With LLM agent
uv pip install -e ".[agent]"

# With REST API
uv pip install -e ".[api]"

# With Streamlit demo
uv pip install -e ".[demo]"

# All features
uv pip install -e ".[all]"

# Development
uv pip install -e ".[all,dev]"

Dependencies

Package	Version	Purpose
z3-solver	>=4.12.0	SMT solver for formal verification
pydantic	>=2.0.0	Data validation
typer	>=0.12.0	CLI framework
rich	>=13.0.0	Terminal output
litellm	>=1.30.0	LLM integration (optional)
fastapi	>=0.109.0	REST API (optional)
streamlit	>=1.32.0	Web demo (optional)

---

CLI Reference

Command	Description
verify-cbl check	Verify single COBOL/Java statement pair
verify-cbl translate	Translate COBOL file to verified Java
verify-cbl compare	Compare existing COBOL and Java files
verify-cbl batch	Batch verify multiple statements
verify-cbl scan	Extract variables from COBOL file
verify-cbl serve	Start REST API server
verify-cbl demo	Run CLI demonstration
verify-cbl demo-streamlit	Start Streamlit web demo
verify-cbl info	Show engine capabilities

Examples

# Translate with Ollama (local LLM)
verify-cbl translate \
  -s tests/industrial_cases/case1_payroll_complex.cbl \
  -o Payroll.java \
  --llm ollama \
  --model deepseek-coder-v2

# Batch verify with JSON report
verify-cbl batch payroll.cbl -o report.json --transactions 5000000

# Compare files for drift
verify-cbl compare --cobol legacy.cbl --java Modern.java -f json

---

Python API

Direct Verification

from decimal import Decimal
from verify_cbl import (
    SymbolicEngine, Variable, NumericType, RangeConstraint,
    CobolComputeParser, SymbolTable, RoundingMode, RoundingOp
)

# Define symbol table
symbols = SymbolTable()
symbols.define("WS-AMOUNT", "9(7)V99")
symbols.define("WS-TAX", "9(6)V99")

# Parse COBOL
parser = CobolComputeParser(symbols)
cobol_expr = parser.parse("COMPUTE WS-TAX ROUNDED = WS-AMOUNT * 0.22.").expression

# Create Java equivalent with truncation
java_expr = RoundingOp(
    operand=cobol_expr.operand,
    scale=2,
    mode=RoundingMode.DOWN  # Java truncation
)

# Define constraints
variables = [
    Variable(
        name="WS-AMOUNT",
        type_=NumericType.DECIMAL,
        constraints=[RangeConstraint(
            min_value=Decimal("0.01"),
            max_value=Decimal("99999.99"),
            decimal_places=2
        )]
    )
]

# Verify
engine = SymbolicEngine(timeout_ms=2000)
result = engine.verify_equivalence(cobol_expr, java_expr, variables)

if not result.is_equivalent:
    ce = result.counter_example
    print(f"Drift at WS-AMOUNT={ce.inputs['WS-AMOUNT']}")
    print(f"COBOL: {ce.output_a}, Java: {ce.output_b}")
    print(f"Difference: {ce.difference}")

LLM Translation with Verification

from verify_cbl import MigrationAgent, MockLLM
from verify_cbl.agent import OllamaLLM

# Demo mode
agent = MigrationAgent(llm=MockLLM(), max_attempts=5)

# Production mode with local LLM
agent = MigrationAgent(
    llm=OllamaLLM(model="deepseek-coder-v2"),
    max_attempts=5
)

result = agent.translate(
    "COMPUTE WS-TAX ROUNDED = WS-AMOUNT * 0.22.",
    "WS-TAX:9(5)V99, WS-AMOUNT:9(7)V99"
)

print(f"Java: {result.java_code}")
print(f"Verified: {result.success}")
print(f"Method: {result.final_method}")  # FORMAL or FUZZING

Full File Translation

from verify_cbl import FileTranslator
from verify_cbl.agent import OllamaLLM

translator = FileTranslator(
    llm=OllamaLLM(model="deepseek-coder-v2"),
    max_math_attempts=5,
)

result = translator.translate_file(
    "legacy.cbl",
    "Modern.java",
    audit_path="audit.json"
)

print(f"Total: {result.statements_total}")
print(f"Verified: {result.statements_verified}")
print(f"LLM-only: {result.statements_llm}")

---

Verification Pipeline

6-Phase Translation Pipeline

flowchart LR
    A[PRE-VALIDATION] --> B[COBOL PARSING]
    B --> C[JAVA GENERATION]
    C --> D[SYNTAX VALIDATION]
    D --> E[FORMAL VERIFICATION]
    E --> F[ERROR DIAGNOSIS]
    F -->|retry| C

Loading

Phase	Description
PRE-VALIDATION	Check COBOL statement and variable definitions
COBOL PARSING	Parse to IR expression tree
JAVA GENERATION	LLM generates BigDecimal code
SYNTAX VALIDATION	Verify Java structure before Z3
FORMAL VERIFICATION	Z3/Fuzzer equivalence check
ERROR DIAGNOSIS	Categorize error for targeted fix

Error Categories

Category	Description	Fix Strategy
SYNTAX_ERROR	Java doesn't parse	Regenerate
WRONG_ROUNDING	Wrong RoundingMode	Specify HALF_UP/DOWN
WRONG_SCALE	Wrong decimal scale	Use PIC clause scale
MISSING_SETSCALE	No setScale() call	Add final rounding
MISSING_OPERAND	Variable omitted	Include all COBOL vars
WRONG_VARIABLE	Unknown variable used	Use only defined vars
CHAINED_CALCULATION	Intermediate rounding	Accept if drift < 0.05

---

Supported COBOL Features

Statements

Statement	Support	Translation
COMPUTE	Full	Direct BigDecimal expression
ADD	Full	Normalized to COMPUTE
SUBTRACT	Full	Normalized to COMPUTE
MULTIPLY	Full	Normalized to COMPUTE
DIVIDE	Full	Normalized to COMPUTE
MOVE	Full	Assignment with scale
IF/ELSE	Full	Nested conditionals
PERFORM VARYING	Full	For-loop translation

Intrinsic Functions

Function	Template	Java Translation
NUMVAL	Yes	new BigDecimal(x.trim())
NUMVAL-C	Yes	Currency string parsing
ABS	Yes	x.abs()
INTEGER	Yes	x.setScale(0, RoundingMode.DOWN)
ANNUITY	Yes	Complex annuity formula
PRESENT-VALUE	Yes	NPV calculation

PIC Clause Semantics

PIC	Interpretation
9(5)V99	5 integer, 2 decimal
S9(7)V9(4)	Signed, 7 integer, 4 decimal
9(2)	Integer only (scale=0)

Rounding Semantics

COBOL	Java	RoundingMode
ROUNDED	setScale(n, HALF_UP)	0.5 rounds up
(none)	setScale(n, DOWN)	Truncation

---

LLM Providers

Provider	Model	Configuration
Mock	Demo	No setup
Ollama	deepseek-coder-v2, qwen2.5-coder	Local: ollama serve
OpenAI	gpt-4-turbo, gpt-4o	OPENAI_API_KEY
Anthropic	claude-3-5-sonnet	ANTHROPIC_API_KEY

# Ollama (recommended for local)
ollama pull deepseek-coder-v2
verify-cbl translate -s legacy.cbl -o Modern.java --llm ollama

# OpenAI
export OPENAI_API_KEY=sk-...
verify-cbl translate -s legacy.cbl -o Modern.java --llm openai

# Anthropic
export ANTHROPIC_API_KEY=sk-ant-...
verify-cbl translate -s legacy.cbl -o Modern.java --llm anthropic

---

Testing

# All tests (421+)
uv run pytest tests/ -v

# With coverage
uv run pytest --cov=src/verify_cbl --cov-report=html

# Specific module
uv run pytest tests/test_translator.py -v

Industrial Test Cases

Case	Scenario	Complexity
case1	Payroll Complex	Taxes, overtime, bonuses
case2	Insurance Premium	Risk factors, compound interest
case3	Loan Amortization	French amortization, APR
case4	Chained Rounding	Sequential rounding operations
case5	Forex Settlement	Multi-currency spreads
case6	Interest Calculation	ACT/365 daily interest
case7	Tax Withholding	Nested IF-ELSE with thresholds
case8	Multi-Currency FX	Bid/ask spread + commission

---

Benchmarks

42 benchmark cases covering realistic COBOL calculations.

Category	Cases	Description
Simple Arithmetic	6	ADD, SUB, chain operations
Multiplication	8	VAT, interest, discount, commission
Division	6	Division by 3, 7, 11 (repeating decimals)
Complex	10	Payroll, insurance, amortization
Edge Cases	12	Rounding boundaries, precision limits

uv run python -m benchmarks.runner --quiet
# Expected: 42/42 PASS, 0 FAIL

Metric	Value
Test Cases	42
Accuracy	100%
Recall	100%
Z3 Timeouts	0 (with HybridEngine)

---

Docker Deployment

Build

# CLI image
docker build -t verify-cbl .

# API server image
docker build --target api -t verify-cbl-api .

Run

# API server
docker run -p 8000:8000 verify-cbl-api

# Health check
curl http://localhost:8000/health

Docker Compose

# API server
docker-compose up api

# With Ollama
docker-compose --profile ollama up api-with-ollama

---

Project Structure

verify-cbl/
├── src/verify_cbl/
│   ├── agent/              # MigrationAgent, LLM providers, diagnostics
│   ├── engine/             # Z3 solver, fuzzing, hybrid engine
│   ├── ir/                 # Expression nodes, constraints, types
│   ├── parsers/            # COBOL/Java parsers, BigDecimal simplifier
│   ├── translator/         # FileTranslator, code generator
│   ├── scanners/           # DATA DIVISION scanner
│   ├── prompts/            # LLM prompt templates (YAML)
│   ├── compare/            # COBOL vs Java comparison
│   ├── cli.py              # Typer CLI (15 commands)
│   └── api.py              # FastAPI REST server
├── tests/                  # 421+ tests
│   ├── industrial_cases/   # 8 real-world scenarios
│   └── cobol_samples/      # 10 COBOL programs
├── benchmarks/             # 42 benchmark cases
├── demo/                   # Streamlit web demo
├── Dockerfile              # Multi-stage build
└── docker-compose.yml      # API + CLI containers

---

REST API

Method	Endpoint	Description
GET	/health	Health check
POST	/check	Verify COBOL/Java pair
POST	/translate	Translate COBOL to Java
POST	/compare	Compare files
POST	/batch	Batch verification

curl -X POST http://localhost:8000/check \
  -H "Content-Type: application/json" \
  -d '{
    "cobol": "COMPUTE WS-TAX ROUNDED = WS-AMOUNT * 0.22.",
    "java": "BigDecimal tax = amount.multiply(new BigDecimal(\"0.22\")).setScale(2, RoundingMode.HALF_UP);",
    "cobol_vars": "WS-AMOUNT:9(7)V99,WS-TAX:9(6)V99"
  }'

---

Configuration

# config.yaml
engine:
  z3_timeout_ms: 2000
  fuzzing_iterations: 100000

agent:
  max_attempts: 5
  chained_drift_tolerance: 0.05

from verify_cbl.config import MigrationConfig
config = MigrationConfig.from_yaml("config.yaml")

---

License

MIT License. See LICENSE.

---

Author

Alessandro Potenza (ap.alessandro.potenza@gmail.com)

---

References

• Z3 Theorem Prover
• COBOL Language Reference
• Java BigDecimal