Program invariants—conditions that must always hold true at specific points in code, such as loop invariants or pre- and post-conditions—are critical for software correctness, security, and formal verification. However, identifying them manually is notoriously tedious, and traditional static analysis tools often struggle with complex logic. This is where artificial intelligence bridges the gap. By handling the cognitive heavy lifting, AI acts as a force multiplier, freeing developers to focus on higher-level system design and creative problem-solving.
There is a difference between asking a machine to find a bug and asking a machine to discover a relationship.
The first question assumes that we already know what we are looking for.
The second does not.
This distinction matters.
Throughout this book we have treated memory safety as a problem of maintaining relationships that C does not necessarily express. A value has a meaning. A size describes an extent. A pointer is expected to identify an object. An offset is expected to remain within that object. An object is expected to remain alive. An owner is expected to remain responsible for it.
The programmer is expected to keep these relationships coherent.
The difficulty becomes obvious when the program is small enough to fit inside a person's head. We can follow a value from its origin through its transformations and eventually to the operation that consumes it. We can ask what must be true at each step.
But real programs are not small.
The relationships are distributed across functions, files, modules, data structures, APIs and years of maintenance. An invariant established in one place may be relied upon somewhere else. Two programmers may use different names for the same concept. The same concept may be represented by several different types. An assumption may exist only because everyone who has touched the code happens to understand it.
This is where AI-assisted analysis becomes interesting.
Not because an AI can answer the questions in this book.
Those questions are already available to the programmer.
The interesting possibility is that an AI can help us discover the questions we did not know to ask.
Consider a codebase containing:
size
length
capacity
count
offset
end
used
availableA programmer looking at one function may understand each variable perfectly.
But perhaps three of them describe the same underlying quantity.
Perhaps one is measured in bytes and another in elements.
Perhaps allocation uses one representation while access uses another.
Perhaps the relationship between them is never expressed anywhere.
The code may nevertheless depend upon the relationship being correct.
An AI could be asked:
Find places where different variables appear to represent the same conceptual quantity. Identify where their representations diverge and where the code assumes that they remain equivalent.
That is a different kind of question.
It does not tell the AI what invariant to look for.
It asks the AI to search for invariants.
The programmer supplies meaning.
The machine searches the program for evidence of that meaning.
The programmer then decides:
Yes. That is the relationship I intended.
Or:
No. That interpretation is wrong.
Only then does it make sense to ask whether the relationship can be expressed as a type, an assertion, a static analysis rule, a test, or some other mechanism.
This suggests a new division of cognitive labour.
The programmer asks:
What is this program supposed to mean?
The AI asks, in effect:
What relationships appear to exist within the program?
The programmer then decides:
Yes. That is the relationship I intended.
Or:
No. That interpretation is wrong.
This changes the role of the AI.
It is not the authority on correctness.
It is not a replacement for the programmer.
It is not even necessarily a vulnerability detector.
It is a machine for exploring the semantic structure of a program.
Consider another question:
Find all functions that create, transform, store, return, or release objects of this type. Construct the apparent lifetime relationships between them. Identify assumptions about lifetime that are not represented in the interfaces.
This is difficult for a human to do exhaustively.
The question is not:
Is there a use-after-free?
It is:
What lifetime model does this subsystem appear to assume?
That distinction is important.
A vulnerability is a conclusion.
An invariant is an explanation.
If the AI discovers that a pointer returned by one subsystem is routinely stored by another subsystem, while a third subsystem can release the underlying object, it may not know whether that is a bug.
But it can expose the relationship:
A returns pointer P.
B retains P.
C can release the object containing P.
No explicit ownership relationship connects B and C.The programmer can then decide what the intended model actually is.
The same approach can be applied to quantities.
Find every path by which an externally supplied count can influence both an allocation size and a later memory access. Identify transformations between the two uses.
Or to object identity:
Find places where a pointer is passed between components. Identify the evidence that each component believes it refers to the same object.
Or to representation:
Find values whose semantic role changes during their lifetime. In particular, identify transitions between elements, bytes, offsets, addresses, capacities and counts.
Or to ownership:
Find resources for which creation, use and destruction occur in different components. Identify the assumptions that connect those operations.
These questions are interesting because they search for structure rather than syntax.
The AI is not looking merely for calls to memcpy, malloc or free.
It is looking for relationships between things.
That is closer to the problem this book has been trying to describe.
There is another useful question:
Find invariants that cross function boundaries.
This can reveal a particularly important class of assumptions.
A function may accept:
buffer
lengthand internally assume:
length <= buffer_capacityThe function's type does not express this.
Its caller may know it.
The implementation may rely upon it.
The documentation may mention it.
Or nobody may have written it down at all.
The relationship nevertheless exists.
It is an invariant maintained socially rather than mechanically.
An AI examining the larger program may be able to identify such relationships by comparing callers, callees, data structures and repeated patterns.
It could then report:
This function appears to require the following relationship:
length <= capacity(buffer)
I found this relationship established explicitly in four callers,
inferred in two callers, and not established in one caller.That is much more useful than:
Possible buffer overflow.The first statement describes the program's apparent semantic contract.
The second merely names a class of failure.
This also suggests another question:
Find invariants that have no obvious owner.
A relationship can be real without belonging to any particular piece of code.
Who is responsible for ensuring that a cached length remains consistent with the underlying object?
Who ensures that an offset remains relative to the object from which it was calculated?
Who ensures that a pointer remains valid after ownership is transferred?
Who ensures that two representations of the same state are updated together?
If the answer is "the programmer", then the program may contain an invariant that exists entirely in human memory.
That is precisely the kind of invariant that is vulnerable to being forgotten.
AI-assisted analysis could therefore become a way of finding the semantic assumptions that have accumulated between the formal structures of a program.
There is an even more interesting question:
Find places where two parts of the program appear to believe different things about the same object.
This might compare allocation code with access code.
Serialization with deserialization.
Initialization with destruction.
A producer with its consumers.
A caller with its callee.
A type definition with the assumptions made by the code manipulating it.
The result need not be a vulnerability.
It might instead reveal an architectural contradiction.
One component may treat a field as a count.
Another may treat it as a byte length.
Both interpretations may be individually reasonable.
Together they are impossible.
The AI has not found the bug.
It has found the disagreement from which a bug might emerge.
This is perhaps the most interesting extension of invariant analysis.
The programmer normally begins with a hypothesis:
I suspect that this is the invariant.
The AI could instead begin with the program itself:
Here are relationships that appear to be repeatedly relied upon.
That reverses the direction of analysis.
Instead of starting from a known invariant and asking whether the program preserves it, we start from the program and ask what invariants appear to exist.
The resulting workflow might look like this:
program
↓
observed relationships
↓
candidate invariants
↓
programmer interpretation
↓
explicit invariant
↓
type, assertion, analysis or testThe important step is the middle one.
The AI proposes.
The programmer interprets.
The program then becomes an opportunity to make the relationship explicit.
This is where AI becomes a different kind of cognitive instrument.
A compiler can enforce a relationship that has been expressed in a form the compiler understands.
A static analyzer can search for violations of rules that have been formulated.
A test can exercise states that someone thought to test.
But before any of these things can happen, somebody has to identify the relationship that matters.
That is often the difficult part.
A programmer can know that a buffer must be large enough.
But what exactly establishes "large enough"?
A programmer can know that a pointer must remain valid.
But what exactly establishes the lifetime?
A programmer can know that two fields must remain synchronized.
But where is that relationship represented?
These questions are not always difficult because the programmer lacks knowledge.
They are difficult because the relationships are distributed across the program.
The possible relationships grow faster than a person can comfortably inspect.
This is where an AI system may have an unusual advantage.
It can examine many representations of the same concept simultaneously.
It can compare names, types, data flow, callers, callees, comments, assertions and repeated patterns.
It can notice that a quantity called count in one place becomes size in another.
It can notice that one component calculates an extent while another independently calculates an access length.
It can notice that ownership appears to change without an explicit transfer.
It can notice that an assumption is documented in one place and contradicted in another.
None of this establishes that the program is wrong.
But it can expose the relationships that deserve human attention.
That suggests a more useful question to put to an AI than:
Is this code secure?Try:
What assumptions does this code appear to depend upon that are not explicitly represented?
Or:
What relationships exist here that are maintained only by convention?
Or:
What concepts appear to have multiple representations in this codebase?
Or:
Where does the program appear to rely upon two values remaining consistent, without mechanically enforcing that consistency?
Or simply:
What invariants have I not thought to ask about?
The last question may be the most interesting of all.
Because if an AI can reliably help us discover invariants that were previously invisible, then its value is not primarily that it finds more bugs.
Its value is that it expands the programmer's field of attention.
The programmer remains responsible for meaning.
The AI helps explore the space of possible meanings and relationships.
The compiler and other formal tools remain responsible for enforcing whatever can be expressed mechanically.
The division of cognitive labour therefore becomes:
Programmer
│
│ intended property
▼
AI-assisted analysis
│
│ candidate invariants / relationships
▼
Programmer
│
│ validated invariant
▼
Language + verification tools
│
│ compile-time / runtime enforcement
▼
Program
This does not eliminate human reasoning.
It changes where human reasoning is spent.
Instead of spending all of our effort discovering what relationships might exist, we may spend more of it deciding which relationships actually matter.
Instead of asking the machine to tell us whether the program is correct, we ask it to show us where the program appears to depend upon something that has never been made explicit.
And that brings us back to the central problem of this book.
Memory safety failures are not merely failures of instructions.
They are failures of relationships.
The most useful AI for programming may therefore not be the one that writes the most code.
It may be the one that looks at a large body of code and says:
I found a relationship here.
I don't think anyone has named it yet.
That is the moment at which an implicit invariant can become an explicit one.
And once we can see an invariant, we can begin to decide what should be done with it.
We can document it.
We can test it.
We can assert it.
We can encode it in an interface.
We can give it to a static analyzer.
We can put it into a type system.
Or, if necessary, we can discover that the program was never actually maintaining it at all.
The machine has not proved the program correct.
It has done something perhaps more useful.
It has helped us discover what correctness was supposed to mean.