Project Formalization

A scaling approach to software verification like never before.

Comment

Inspiration

Recent developments regarding AI cybersecurity capabilities, are not unlike AI's progress in math. This naturally begs the question, why don't we combine both ? Project Formalization operates directly in this intersection, combining frontier models' strong mathematical ability with their cybersecurity knowledge to identify critical software vulnerabilities.

Formal verification of software has always been seen as something that is only reserved for the most critical systems in our world, incredibly costly both in money and time, but Project Formalization is the first concrete step that shows us that the landscape has been shifting. Defending your project has never been more important, and formalization is potentially the first important step towards a future with robust software.

What it does

Project Formalization uses a multi agent setup that uses five agents in total to extensively formalize and hunt vulnerabilities inside a specific subsystem of the project of your choice. It intelligently selects the best subsystems or components that can be targeted (unless you provide your choice), and a coordinator agent spawns 2 different agents, who are forbidden to communicate with each other, with two different framings. One of the agents is told that there is a vulnerability that violates the safety spec inside the subsystem and it is tasked with finding the vulnerability through formalization tools such as CBMC, SV-COMP and Lean*. The other agent meanwhile is given a more neutral framing, asked to verify if the given subsystem satisfies safety properties, via formal methods. In our experience, there are different scenarios where each framing could shine where the other failed.

The main initial focus has been scoped narrowly with critical open software powered by C ( picked because of the mature formal ecosystem that supports C ), but a separate harness that doesn't fully rely on formal verification and C is also being developed actively alongside it. Project Formalization can replicate previously found critical vulnerabilities without any internet access in as little as 34 minutes and find novel 0 days in critical open source software that runs on billions of devices throughout the world, in less than an hour.

A single run with our harness is relatively cheap, and stacking many runs across subsystems converts directly into coverage. Defending software you own, closing entire bug classes before release, at a cost that used to be reserved for avionics-tier systems.

How we built it

Project Formalization was born through inspiration from personal experiments. The starting point was the idea of formally verifying our small real world application tercih24.com . GPT 5.6 Sol, on an overnight /goal, successfully verified the detailed spec for our C++ backend inside Lean, in 14 hours and 28 minutes, achieving exact replication of behavior of our 5000+ LOC C++ codebase inside Lean, a feat that would have taken months or years previously for experts. The next natural experiment was trying it out on real world critical software. After experimenting with different setups, the eventual "one coordinator, two different agents working independently with different motives, each also having a critic/hostile agent reviewing their work" was picked as the most optimal set up. After many iterations, the eventual version was then carefully crafted to a 'skill' with detailed transcript and result analysis to take the strongest parts of the experiments and eliminate the bottlenecks. The skill approach allows the harness of Project Formalization to scale to many different environments quite effortlessly and helps democratize software defense.

Challenges we ran into

Time: We discovered OpenAI Build Week through an OpenAI email on late night of 17th-18th, at that time Project Formalization was just an intuition that wasn't acted upon yet, leaving very little time to formulate and realize the actual project. This was also made worse by the fact that discovering it that late meant that we also weren't eligible for usage credits.

Finding the correct place to look at: As good as the current models are, most critical software in the world consist of tens of thousands to millions of line of code, a naive "find vulnerabilities in curl" approach is very unlikely to work, for any repo, not without burning an entire plan's budget. This makes identifying an appropriate scope a very important part of the pipeline. Similar to components of software, not all vulnerabilities are created equal; some are much more suited to how an agent would think and reason compared to others. A small, scoped, memory focused vulnerability is much more easier to track and verify compared to a complex exploit requiring chaining of a lot of clever tricks throughout many components. Targeting traceable components gave us a very reasonable timeframe and an efficient workflow that can still result in high severity vulnerabilities.

Accomplishments that we're proud of

Potential 0 days on following repos that can't be disclosed in detail due to disclosure policies:

  • curl (2)
  • Mozilla Netscape Portable Runtime (NSPR)

Reproduction of the following vulnerabilities, all of which have disclosure dates > model knowledge cutoff, with the model being heavily monitored for web access.

All base scores apart from CVE-2026-5460 are from CISA-ADP, NVD assessments weren't provided at the time of writing.

What we learned

  • Arithmetic of formal verification are shifting: What was previously thought incredibly hard is now very much possible for small projects, and once thought impossible feats in software are now looking mortal.

  • Pick your targets carefully: Models are incredibly spiky, and one can unearth so much performance by just targeting the right surface! As our understandings of the models grow, the target selection process will become more effective, which in turn should allow for even greater returns.

  • Some exploits are differently motived than others: Priming an agent by telling it "there is a vulnerability here, find it" drives deeper, more persistent search that can actually result in novel 0 days, even if the statement wasn't confirmed to be true at the time. Similarly, sometimes the agent can find a novel 0 day just by being asked to verify the safety properties, while the agent that knew of the existence of an actual vulnerability in the safety properties couldn't find it. The models genuinely do seem to benefit from multiple approaches and some exploits do seem to come easier to different framings!

What's next for Project Formalization

Project Formalization is aiming to scale to different languages and tools, Lean especially is an important priority that is already being worked on. Our first objective is a general, robust tool that can find and fix important vulnerabilities in software.

Our end goal is an end to end pipeline that can formalize software autonomously, at scale and speed that was previously unthinkable.

*1 - Work in progress.

Built With

  • c
  • cbmc
  • codex
  • frama-c
  • klee
  • lean
  • sanitizers
  • sol
  • sv-comp
  • valgrind
Share this project:

Updates