Core Verification
Cobalt COBOL
Formal proof for legacy mainframe systems.
Formal vulnerability analysis for COBOL programs running on mainframe and mid-range systems. Cobalt COBOL transpiles COBOL to a verifiable intermediate representation, then applies Z3 to prove arithmetic overflow, division-by-zero, dead code paths, and logic errors in business-critical batch processing. Built for banks, insurers, and government agencies that cannot rewrite — only harden.
800B+
Lines in Prod
10
Construct Classes
100%
Proof Rate
§ SPECIFICATION
Input
- COBOL source (.cbl, .cob)
- Copybooks and data division definitions
- Optional: JCL batch job definitions
- Optional: VSAM / DB2 schema for data flow analysis
Constraints Verified
- Integer arithmetic overflow in COMPUTE statements
- DIVIDE BY ZERO reachability (DIVIDE INTO / DIVIDE BY)
- Dead code via provably false condition branches
- Buffer overrun in MOVE operations with mismatched PIC clauses
- Numeric truncation in PIC 9 to PIC 9 assignments
- Loop termination proofs for PERFORM UNTIL constructs
Output
- Z3 proof artifact per vulnerability class
- COBOL→Python transpilation trace
- Arithmetic overflow witness with exact operand values
- Dead code certificate (formally unreachable paths)
- Remediation patch in original COBOL syntax
§ SAMPLE PROOF ARTIFACT
ARTIFACT // COBOL-DIV-01FAILURE DETECTED
// SAMPLE PROOF — COBALT COBOL ENGINE
Mainframe payroll — DIVIDE INTO overflow on zero divisor
TargetLegacy payroll COBOL batch job
Condition
WS-HOURS-WORKED = 0 → DIVIDE WS-TOTAL-PAY INTO WS-HOURS-WORKED → division by zero, program abendVerdictSAT
SummaryDivision by zero reachable under zero-hour employee record. Z3 witness: WS-HOURS-WORKED=0. DIVIDE INTO finding confirmed across 2,345 NIST+GnuCOBOL benchmarks.
StatusReview-ready
§ FIELD VALIDATION
| # | Target | Vulnerability Class | Status |
|---|---|---|---|
| 01 | NIST COBOL Suite DIVIDE INTO overflow | DIVIDE INTO overflow | 100% Proof Rate |
| 02 | GnuCOBOL 3.2 Dead Code Paths | Dead Code Paths | Formally Proven |
| 03 | Legacy Payroll Arithmetic Overflow | Arithmetic Overflow | CVE Filed |
Run Cobalt COBOL on your system.
Formal engagement starts with a technical intake. We scope, configure, and deliver a proof artifact within the agreed SLA.