AI is becoming surprisingly good at finding security vulnerabilities in code.

Give a modern LLM a function containing an integer overflow, a use-after-free, or a suspicious bounds check, and it may identify the problem in seconds. Give an AI agent access to an entire repository and it can search call sites, inspect data flows, generate tests, and propose patches.

So a natural question appears:

If AI becomes good enough at vulnerability research, do we still need formal methods?

I think the answer is yes — perhaps more than ever.

AI and formal methods solve fundamentally different parts of the problem. AI is excellent at generating security hypotheses. Formal methods are excellent at determining whether precise properties actually hold.

The most interesting future is therefore not AI versus formal methods, but AI combined with formal methods.

AI Thinks Like a Security Researcher

Consider this simple C function:

void *allocate_records(int count, int record_size)
{
    if (count <= 0 || record_size <= 0)
        return NULL;

    int size = count * record_size;

    return malloc((size_t)size);
}

A security researcher will immediately become suspicious of:

int size = count * record_size;

If both values are large enough, the multiplication can overflow. In C, signed integer overflow is undefined behavior.

Modern AI models are often able to notice exactly the same thing.

But AI can go much further than matching a local pattern. It can inspect callers, understand comments and API documentation, infer what the developer intended, search for attacker-controlled inputs, and reason about whether the bug could become exploitable.

This makes AI particularly interesting for vulnerability research.

Many security vulnerabilities are not simply “an invalid memory access at line 42.” They emerge from interactions between components, incorrect assumptions, missing authorization checks, protocol state machines, or subtle misuse of APIs.

These problems require context.

And context is precisely where LLMs can be extremely useful.

But AI Is Still Probabilistic

There is an important difference between saying:

“This multiplication looks vulnerable.”

and:

“For the defined input domain, this multiplication can never overflow.”

The first is a security hypothesis.

The second is a property that can potentially be proved.

An LLM may correctly identify the overflow in one run and miss it in another. It may incorrectly assume that callers restrict count, misunderstand an API contract, or report a vulnerability on a path that is actually unreachable.

This is not necessarily a defect in AI. It follows from how these systems work.

AI reasoning is probabilistic and heuristic. Its strength is its ability to reason across enormous amounts of imperfectly structured information.

But security assurance sometimes requires something stronger than a plausible answer.

This is where formal methods enter the picture.

Formal Methods Ask a Different Question

A formal analyzer does not ask whether the multiplication looks dangerous.

It reasons about the possible values of count and record_size under a defined model.

For example, if the environment allows:

1 <= count <= 1,000,000
1 <= record_size <= 4096

the analyzer can reason about the complete value ranges rather than trying a collection of representative inputs.

If overflow is possible, the analysis can identify the conditions that lead to it.

If the constraints instead guarantee that the multiplication remains within the range of int, a sound analysis can establish that this particular undefined behavior cannot occur within the modeled assumptions.

That is fundamentally different from testing — and from asking an LLM.

As discussed in my previous posts on undefined behavior and fuzzing, exhaustive reasoning is one of the main advantages of formal methods.

But formal methods also have an important limitation.

They need us to ask the right question.

Formal Verification Is Only as Good as the Property

Imagine a payment function that correctly checks memory accesses, integer ranges, and pointer validity.

The implementation may be completely free of undefined behavior.

But what if the developer simply forgot to check whether the user is authorized to perform the payment?

Memory safety verification will not magically invent the missing security requirement.

This distinction is important.

Formal methods can provide very strong guarantees about properties represented by the analysis. They do not automatically understand every security requirement that humans forgot to specify.

AI has almost the opposite strength.

An LLM reading:

transfer_money(source, destination, amount);

may notice that every neighboring endpoint performs an authorization check while this one does not.

It can infer an implicit requirement from the surrounding code.

It cannot prove the implementation correct.

But it may discover what should be proved.

That makes the two approaches surprisingly complementary.

AI as the Assistant, Formal Methods as the Foundation

TrustInSoft describes this idea as using AI as an assistant and formal methods as a foundation.

I think this architecture is particularly interesting for vulnerability research.

A future security workflow could look like this.

1. AI explores the attack surface

An AI agent scans the repository and identifies potentially interesting areas:

Instead of asking a human researcher to manually inspect thousands of functions, AI helps prioritize where to look.

2. AI generates security hypotheses

The model might report:

count * record_size may overflow before being converted to size_t.

Or:

This pointer appears to remain reachable after the object has been freed.

Or even:

This operation seems to be missing the authorization check used by similar endpoints.

These are not proofs.

They are questions worth investigating.

3. Formal analysis checks what can be formalized

For properties such as integer overflow, invalid memory accesses, null dereferences, invalid shifts, or violations of explicit invariants, formal methods can take over.

The AI hypothesis becomes a proof obligation.

Now the result no longer depends on whether the model “feels confident.”

The analyzer determines whether the property holds under the specified assumptions.

4. AI helps build the verification environment

Historically, one obstacle to formal verification has been the engineering effort required to prepare an analysis: drivers, stubs, assumptions, contracts, and models.

This is exactly the kind of repetitive work AI can accelerate.

TrustInSoft Analyzer, for example, introduced AI-assisted generation of analysis drivers and context-aware stubs in 2026. The AI helps prepare the analysis, while the formal analyzer still performs the verification itself.

This separation is important.

AI improves productivity.

Formal methods provide the guarantee.

5. Feed the result back to AI

Suppose the formal analysis confirms that an overflow is reachable.

The result can be fed back to the AI agent.

The AI can then:

The formal analyzer runs again on the modified code.

The loop becomes:

AI hypothesis
      ↓
Formal analysis
      ↓
Counterexample / proof
      ↓
AI interpretation and remediation
      ↓
Formal verification

This is much more powerful than simply asking an AI model whether the code is secure.

From Bug Detection to Security Assurance

AI will almost certainly become better at vulnerability discovery.

It can already process code faster than a human reviewer, correlate information across large repositories, generate fuzzing harnesses, and suggest attack scenarios.

Formal methods solve a different problem.

They provide deterministic reasoning about defined properties and can establish the absence of certain classes of errors across the modeled state space.

Neither approach is sufficient for every security problem.

AI can understand context but cannot provide mathematical certainty.

Formal methods can provide mathematical certainty but only about properties represented by the model and specification.

Humans still define what “secure” actually means.

That leads to a useful division of responsibilities:

AI finds what looks suspicious.

Formal methods determine what can be proved.

Humans decide whether we are proving the right security properties.

The future of vulnerability research may therefore not be autonomous AI replacing security researchers or formal verification replacing testing.

It may be a continuous collaboration between human reasoning, AI exploration, dynamic testing, and formal verification.

AI gives us scale.

Formal methods give us guarantees.

Together, they may allow us to investigate more code — while trusting the conclusions much more than either approach could achieve alone.