Project Formalization pairs a frontier model's mathematical ability with formal verification to hunt critical vulnerabilities in the software that runs on billions of devices, reproducing known CVEs in as little as 34 minutes, offline, and surfacing novel 0-days in under an hour.
Proof. Formally verifying software, mathematically proving a program cannot misbehave, has long been reserved for the most critical systems we build, because it cost more time and money than almost anyone could justify.
The same trajectory that took AI from struggling with competition math to solving it is now reaching software. What was recently expert-only and painfully slow is becoming fast and routine for small, well-scoped targets. Project Formalization is a concrete step into that intersection: frontier mathematical reasoning, pointed at real cybersecurity surfaces, with formal methods as the ground truth.
A coordinator scopes the project and picks the subsystem worth attacking, or you hand it one directly. It then spawns two agents that are forbidden from communicating. Each is shadowed by a hostile critic that tries to tear its reasoning apart. Five agents in total, working the same code from irreconcilable premises. Only communication is with the coordinator.
The initial focus is narrow on purpose: critical open-source C, chosen for its mature formal ecosystem. A separate harness that doesn't lean fully on formal verification or C is in active development alongside it.
The whole thing is packaged as a portable skill, so it moves across environments cheaply. A single run is inexpensive; stacking runs across subsystems converts directly into coverage, closing entire bug classes before release, at a cost once reserved for avionics-tier systems.
Every reproduction below has a disclosure date after the model's knowledge cutoff, run with web access heavily monitored, and several with no internet at all.
| Target | CVE | Severity |
|---|---|---|
| curl v8.20 | CVE-2026-10536 | 9.8 CRITICAL |
| curl v8.20 | distinct UAF | USE-AFTER-FREE |
| wolfSSL v5.9.1 | CVE-2026-55960 | 7.5 HIGH |
| wolfSSL v5.9.1 | CVE-2026-6679 | 7.5 HIGH |
| wolfSSL v5.9.2 | CVE-2026-5460 | 6.5 MEDIUM |
Severity scores from CISA-ADP, except CVE-2026-5460. NVD assessments were not yet published at time of writing.
Undisclosed pending responsible-disclosure timelines, reported here only by target.
Netscape Portable Runtime ships inside browsers and TLS stacks across the ecosystem.
The findings didn't come from a single strategy. The falsifier's certainty produced 0-days even where no bug was confirmed. The verifier's attempt to prove safety surfaced counterexamples the falsifier couldn't reach.
Different exploits are, in a real sense, differently motivated. Running both premises in parallel is where the coverage comes from.
An overnight /goal proved a 5,000+ LOC C++ backend behavior-exact inside Lean, in 14 h 28 m. A feat that used to take experts months, or years.
What was thought incredibly hard is now very doable for small projects, and once-impossible feats in software are starting to look reachable.
Models are spiky. “Find vulnerabilities in curl” burns a whole budget for nothing; a small, traceable, memory-focused surface returns high-severity results in a sane timeframe. Target selection is half the pipeline.
Telling an agent a bug exists drives a deeper search. Telling another to merely verify safety surfaces different bugs. The model genuinely benefits from being approached from more than one side.
Just fetch the skills from the repo and you are good to go!