01 / The outcome
Verify the behavior. Find what matters.
Using formal methods, AxiomCode helped identify and address several defects in widely used software across Spring Boot, Spring Cloud, and Keycloak. In Spring Cloud Config, one led to a critical issue rated 9.1 out of 10 on CVSS; in Keycloak, a cascading failure revealed information about the server behind an identity service.
The work started with a code-verification question: does this program actually respect the boundaries its developers intended? Answering it meant following behavior across functions, checking how values changed, and connecting those changes to an observable result.
Some of our findings had security consequences. The capability behind them is broader: understanding how code behaves as a connected system. That is the foundation of our work on formal verification for AI software engineering.
02 / Spring · 9.1 / 10
Spring Cloud: a small assumption, a critical consequence.
9.1/10CVSS 3.1 · Critical
Spring Cloud Config supplies application settings from a central server. In the code path we investigated, a request included a label used to locate those settings. One function transformed the label; a later function used the transformed value to construct a file location. The missing check was whether that location still belonged inside the intended directory.
Think of a delivery address being rewritten after it has passed reception. The next person trusts the approved address, even though it now points somewhere else. Here, that mismatch could let a request reach files the server was never meant to return.
AxiomCode connected the input transformation, repository lookup, and file-handling behavior into one explanation. Our investigation also followed what happened next: returned files could expose sensitive data, and configuration placeholders in those files could resolve to live secrets. An invalid location could also reach an unhandled server-error path. The value was in showing how the pieces combined, then identifying where to break the chain.
Follow the value as its meaning changes across the codebase.
An input gets through
A request supplies a label that selects which configuration version to load.
Label = a branch or tag; in this case, an SVN directory.
Its meaning changes
Decoding turns part of the label into path separators.
A boundary is crossed
The resolved path can escape the repository, exposing readable files and potentially secrets.
Does the final file location still belong to the intended repository?
Two possible outcomes from the same path
File and secret exposure
Returned files can expose sensitive data. Configuration placeholders in those files may also resolve to live secrets.
An unhandled error can escape
The application can return a server error instead of a controlled response.
Conceptual illustration of the reported investigation, not a literal call graph or a proof of every possible execution path.
Spring’s May 6 advisory credits AxiomCode’s use of AxiomEngine alongside other reporters. The project shipped fixes, including the open-source 5.0.3 and 4.3.3 releases. Our repair priorities focused on checking values after transformation and enforcing the allowed directory before file access.
03 / Why it mattered
The impact extends beyond one repository.
Broadcom reports that the Spring and Java ecosystem is relied on by over half of the Fortune 500. That indicates the scale of the ecosystem; exposure to this particular issue depends on the affected Config Server versions and deployment.
Configuration servers sit close to the settings that keep applications running. A boundary failure there can expose sensitive files and configuration, with consequences for the services that depend on them. For engineering teams, this made the finding an upgrade priority, not just an interesting code defect.
The issue entered the wider public response: Canada’s Cyber Centre listed it in a Spring advisory, France’s CERT-FR included it in its weekly roundup of significant vulnerabilities at 9.1, and HeroDevs published a dedicated analysis. These are independent records of the issue and its importance to software operators.
The practical result was a previously hidden behavior made visible, a public report that teams could act on, and fixes available from the maintainers. That is the kind of impact code verification should deliver.
04 / Keycloak · The cascade
Keycloak: one weakness made another observable.
Keycloak handles identity and login for applications. An administrator with permission to manage a realm—a group of users and applications—could configure a file containing signing keys. That legitimate setting could reach file loading outside a sufficiently restricted directory.
The next step made this more than an unchecked file path. The application reacted differently depending on whether a file existed and could be read. Those differences let a caller learn about files on the host without seeing their contents. A configuration choice, a filesystem operation, and a response combined into a leak of information.
AxiomCode traced that cascade and helped move the issue toward remediation. The fix needed to restore the boundary between realm-level configuration and server-level files. Hiding one error message would leave the underlying behavior in place.
The problem emerges when configuration, file access, and responses connect.
A permitted setting
An administrator supplies a keystore path for their realm.
A wider reach
The path can point beyond that realm’s intended files.
An observable difference
The server’s response changes with the state of the file.
Can a realm-level setting reveal something about a host-level file?
Different file states become clues
Missing
No file at this path
Not readable
A file cannot be opened
Readable
A file can be opened
The information leak is the difference. Repeated observations can reveal where files exist and which are readable — without exposing their contents.
Conceptual illustration of the reported investigation, not a literal call graph or a proof of every possible execution path.
Red Hat acknowledges AxiomCode’s report as CVE-2026-9083. Keycloak introduced realm-specific keystore directories; later, its 26.7.3 release addressed an incomplete-fix variant. That repair history reinforces the engineering lesson: verify the resolved location and the resulting behavior, including variations a first patch may miss.
05 / What made it possible
Connected context becomes evidence for a fix.
The graph builder gives the investigation a map: where a value comes from, which functions handle it, and which operations it can reach. AxiomEngine uses that structure to examine the assumptions along the route. Is the value still valid after it changes? Does the next operation remain within its intended boundary? What can the caller observe?
For Spring, the missing connection was between a transformed label and the file it could reach. For Keycloak, it was between a configured path and the information exposed by the response. In both cases, the result was an inspectable account of the starting condition, the failure chain, and the checks a repair needed to restore.
Code graph
Connect the code, its inputs, and the operations they reach.
AxiomEngine
Check how those connected operations behave together.
Evidence for a fix
Explain the failure path and the checks it needs.
A simplified view of the investigation: connect a path, check its behavior, and explain the result.
Our pre-disclosure evaluations
In our internal evaluations before official disclosure, the Claude Code workflows we tested—including Security and Code Review—along with Snyk and Semgrep did not surface these same failure chains. AxiomCode did. This describes those evaluations, not a comprehensive benchmark or a claim about the tools’ current capabilities.
06 / Beyond these two cases
More code needs more verification.
AI coding agents make it easier to produce a change. Engineers still need to know what that change does beyond the edited lines. A local improvement can alter assumptions in another component; an apparently reasonable patch can leave an unexpected path open.
These two cases demonstrate the value of following those consequences across a real codebase. The outcome is concrete: publicly acknowledged findings and upstream remediation. The approach gives engineers evidence to review, a reason for the proposed repair, and a clearer idea of what to verify next.
Our direction is formal verification for AI software engineering: make the relationship between code, behavior, and intended constraints easier to examine before software reaches users. Spring and Keycloak are early, practical examples of why that work matters.
07 / Build with us
Give every change a stronger foundation.
AxiomCode Graph is the starting point: structured, connected code context. AxiomEngine builds on it for deeper verification. If your team is exploring how to verify AI-assisted changes, join our early-access waitlist and tell us what you are building.