Core Verification

Cobalt

Formal proof for critical infrastructure.

Formal verification engine for C, C++, RTOS, embedded systems, and cryptographic libraries. Cobalt identifies vulnerabilities with formal evidence under defined execution conditions — not guessed through heuristics. Every finding is backed by a Z3 constraint proof showing the exact input that triggers failure.

25+

Confirmed CVEs

Vuln Classes

Target Domains

§ SPECIFICATION

Input

C / C++ source code or binary
RTOS firmware images
Build configuration + compilation flags
Optional: threat model / attack surface definition

Constraints Verified

Buffer boundary invariants
Integer arithmetic overflow conditions
Null pointer dereference paths
Use-after-free reachability
Format string injection paths
Cryptographic timing side-channels

Output

Z3 SMT-LIB2 proof artifact per finding
Vulnerability class + CWE mapping
Exploitability analysis with witness values
Remediation path with formal verification of fix

§ SAMPLE PROOF ARTIFACT

ARTIFACT // COBALT-WOLF-01FAILURE DETECTED

// SAMPLE PROOF — COBALT ENGINE

wolfSSL DH key parsing — integer overflow

TargetwolfSSL 5.6.x

Conditionkey_len = 0xFFFFFFF4 → alloc_size wraps to 4 bytes

VerdictSAT

SummaryHeap write-out-of-bounds. PR merged upstream.

StatusReview-ready

→ View full artifact repository

§ FIELD VALIDATION

#	Target	Vulnerability Class	Status
01	wolfSSL Integer Overflow	Integer Overflow	PR Merged
02	NASA cFS Stack Overflow	Stack Overflow	ACK Amazon
03	Mosquitto Buffer Overflow	Buffer Overflow	2× CVE Filed
04	libupnp Stack Overflow	Stack Overflow	CVE-2026-41682
05	lwIP Integer Overflow	Integer Overflow	CVE Filed
06	Mongoose Buffer Overflow	Buffer Overflow	CVE Filed
07	llama.cpp Heap Overflow	Heap Overflow	CVE Filed
08	Mozilla NSS Timing Channel	Timing Channel	Fixed

Run Cobalt on your system.

Formal engagement starts with a technical intake. We scope, configure, and deliver a proof artifact within the agreed SLA.

Request Briefing →