← BACK TO WICK § PROOF ARTIFACTS
Not reports.Machine-verifiable evidence. Each artifact is a structured proof showing the vulnerability class, the constraint evaluated, the code path analyzed, and the formal verdict — SAT (exploitable) or UNSAT (failure class ruled out). Z3 4.12 · SMT-LIB2 format.
All Cobalt The Answer
wolfSSL
Integer Overflow → Heap Buffer Overflow
CONDITION
key_len = 0xFFFFFFF0NASA cFS
Integer Overflow in Task Stack Allocation
CONDITION
stack_size > OS_MAX_TASK_STACK_SIZE (unchecked)Eclipse Mosquitto
Buffer Overflow in MQTT PUBLISH parsing
CONDITION
remaining_length crafted to overflow recv bufferlibupnp / pupnp
Stack Buffer Overflow in SOAP response parsing
CONDITION
SERVICE_TYPE header > 512 bytes (no bound check)
CVE-2026-41682
▼ Z3 OUTPUT
COMPAS Recidivism Algorithm
Causal Bias — Protected Attribute Influence
CONDITION
race ∈ {African-American} → risk_score ≥ HIGH with p > 0.65llama.cpp
Heap Buffer Overflow in GGUF metadata parsing
CONDITION
n_kv > UINT32_MAX / sizeof(gguf_kv) — wrap in calloc