As is often the case these days, my poor old noggin is jam-packed with myriad meandering musings pertaining to AI. For example, I just started reading Road Kill by Dennis E. Taylor (you may remember Dennis as the author of We Are Legion (We Are Bob)).
In Road Kill, three twenty-something friends—Jack, Natalie, and Patrick—come into possession of an alien spaceship in the form of an invisible (cloaked) flying saucer. This all starts when Jack inadvertently runs over the ship’s original alien owner, killing “him.” Since the alien was itself cloaked, this really wasn’t Jack’s fault.
The spaceship is controlled by a somewhat snippy AI. Although this AI is obliged to follow our heroes’ orders, it’s not happy about it and refers to them using terms like “semi-sentient pond scum.” As a result, they tell the AI that its name henceforth will be Sheldon.
The first thing Jack and friends do is get Sheldon to fly them to the Moon so they can visit the site of the original Apollo 11 landing. Based on the spaceship’s advanced antimatter-powered technology, this trip takes just 20 minutes or so. On the way, Sheldon “prints” spacesuits for them so they can take a stroll on the lunar surface. Next, they take a quick trip to Mars and still make it back home in time for supper.
I know that the chances of something like this happening to me are infinitesimally small—although I prefer to think of them as “non-zero”—but still, I dream.
Something else I did recently was rewatch the Dot and Bubble episode of Doctor Who. In this thought-provoking story, we discover a domed city full of young adults, each of whom experiences the world through an AI-powered social media interface that’s projected as holographic “bubbles” around their heads. In a scene that’s reminiscent of the overweight humans who can’t move without their floating couches in Wall-E, we find the people in Dot and Bubble can’t navigate through their world without their AI-generated holographic arrows and associated instructions (“Walk forward, turn left…”).
Another AI-related topic that’s weighing on me is software and cybersecurity. There are a couple of aspects to this that seem to be stuck in my mind. The first is the “ancient libraries” phenomenon. This refers to outdated, forgotten, or undocumented software components, data, and legacy systems that remain active in modern IT infrastructures.
In the same way that ancient libraries (like Alexandria) contained vast amounts of knowledge that became vulnerable to decay, loss, or intentional destruction, modern “ancient libraries” of code (libraries, modules, dependencies) are often forgotten, unpatched, and unprotected, thereby creating massive security gaps.
As a somewhat related issue, there’s the “Ship of Theseus” concept. This is a philosophical thought experiment that asks whether an object, like a ship, whose individual components have been replaced over time, remains fundamentally the same object. This leads me to think about computer code that might have been written in the mid-1970s, modified hundreds of times by different people over the years, and yet still contains fragments of the original logic and structure. Even if the underlying code isn’t identical, function calls, data structures, and system interfaces may be conceptually the same as those of the 1970s design. So, is it still the same code?
Today’s code dependence chains are brutal. A modern application might rely on 100+ libraries, which themselves depend on 1,000+ more. Somewhere in the depths of this library tree is code that was written when memory was measured in kilobytes, security wasn’t a priority, and everyone was still figuring things out as they went along.
What we are left with are collections of codebases with 50+ years of accumulated logic and layers built on 1970s design assumptions, 1980s extensions, 1990s networking, and 2000s security patches. All of this can contain bugs and vulnerabilities stemming from a mix of ancient design quirks, edge cases no one ever exercised, and assumptions that are no longer valid.
In many cases, there’s been an attitude of “If it ain’t broke (even though it might be), don’t fix it.” Old code often has known behavior, has been patched repeatedly and extensively, and is considered (hoped) to be stable.
Even though this old code may still contain latent bugs that nobody ever triggered, rewriting it is dangerous. Replacing a core library can break subtle assumptions, introduce new bugs and vulnerabilities, and require extensive retesting. As a result, engineers tend to patch, wrap, and work around rather than replace.
The reason I mention this here is that the folks at Anthropic have built a new class of AI systems—most notably a model called Mythos—that can read, reason about, and actively test software to uncover bugs (including serious, previously unknown “zero-day” vulnerabilities) at a scale and depth that humans simply can’t match.
Unlike traditional tools (static analyzers, fuzzers…), this isn’t just pattern matching. The new systems read code like human researchers, form hypotheses about possible vulnerabilities, and execute the code to test those hypotheses.
The scale and effectiveness of these systems are shocking. Even in its early testing, Mythos has reportedly found thousands of vulnerabilities in widely used systems, including operating systems and browsers. More striking still, it’s uncovering decades-old flaws buried deep in critical software and infrastructure that no one ever noticed. This is why we’re starting to hear phrases like “bugmageddon”; not because each bug is catastrophic on its own, but because the sheer volume is overwhelming.
Because this technology is so powerful, the folks at Anthropic have limited access to ~40 major companies (e.g., Apple, Google). They’ve also launched initiatives like Project Glasswing to use it defensively. The reason for their caution is that the same capabilities that help defenders can also help attackers to dramatically compress discovery times, generate working exploits, and outpace patch cycles, meaning vulnerabilities are found faster than they can be fixed.
But none of this is what I wanted to talk about.
The thing that’s brought AI in general, and software security in particular, to the forefront of (what I laughingly call) my mind is that I just had a very interesting chat with Caroline Guillaume, who is the CEO of TrustInSoft. I last conversed with these little scamps back in 2021 (seeIf You Can’t Trust TrustInSoft, Who Can You Trust?), and a lot has changed since then, let me tell you.
At its heart, the TrustInSoft Analyzer (TISA) is a software verification tool, but that description doesn’t really do it justice. Most traditional tools either scan code looking for suspicious patterns (static analysis) or execute the code with selected inputs (dynamic testing). The problem is that subtle, high-impact bugs—especially memory safety issues like buffer overflows, use-after-free, and integer overflows—tend to slip through the cracks. They either don’t match known patterns or lie dormant, waiting for just the wrong sequence of events to bring the system crashing down around our ears.
All I know is that I want any safety-critical software that in any way affects me and mine to have been verified by the TrustInSoft Analyzer (Source: TrustInSoft)
What the TISA does differently is apply sound formal methods, meaning it doesn’t guess and it doesn’t miss. Instead of testing a handful of inputs, it effectively evaluates all possible values and execution paths at once. As Caroline explained, the tool propagates abstract values through the code while modeling how the underlying hardware handles memory, right down to bit widths, address spaces, and access rules. The result is a mathematically rigorous analysis that can uncover bugs that would never show up in testing, even after tens or hundreds of thousands of runs.
The payoff is profound. These memory safety issues are not just theoretical; they sit at the root of some of the most expensive and dangerous failures in computing, from cybersecurity exploits to system crashes in safety-critical environments. Traditional tools may find some of these problems, but only formal methods can guarantee that none have been missed. And that’s the real differentiator: not “we found some bugs,” but “we can prove the absence of an entire class of bugs.”
Now, here’s where things get especially interesting. Formal methods have long been regarded as the “gold standard” for software verification, but also as something of a specialist sport, requiring significant effort and expertise to set up and use effectively. This is where TrustInSoft’s new AI integration comes into play, and it’s a rather elegant marriage of two very different worlds.
TrustInSoft Analyzer flaunts its new AI integration (Source: TrustInSoft)
AI is being used to automate the “grunt work,” specifically, generating the test drivers and stubs needed to analyze real-world code. In the latest release, this can be done with a one-click, context-aware setup, dramatically reducing the time and effort required to get started. In other words, AI handles the “busywork,” allowing engineers to focus on the results rather than the setup.
What makes this combination so powerful is that the roles are clearly defined. AI brings speed and efficiency, but it doesn’t inherently guarantee results (it can miss things and doesn’t always explain its reasoning). Formal methods, on the other hand, are slower but mathematically rigorous, providing complete coverage and full traceability. By combining the two, TrustInSoft effectively delivers the best of both worlds: rapid setup and iteration, backed by proof that the results are sound, consistent, and complete. As Caroline put it, “AI and formal methods are not competitors; rather, they are very good companions.”
Another major development is the addition of Rust support alongside C and C++. Rust has been gaining serious traction in recent years, largely because of its built-in memory safety features. Many developers are turning to Rust specifically to avoid the kinds of vulnerabilities that plague traditional C/C++ codebases.
However—and this is an important “however”—Rust is not a magic wand. While it eliminates many classes of memory errors, it still allows for “panics” (essentially controlled crashes), arithmetic overflows, and, in its “unsafe” regions, the same kinds of low-level issues found in C and C++. Moreover, real-world systems rarely exist in a vacuum. They are typically composed of modules written in different languages, often by different teams or even different organizations.
This is where TrustInSoft brings something genuinely unique to the table. It doesn’t just analyze C, C++, and Rust in isolation—it understands how they interact. When a Rust module interfaces with legacy C code, for example, any safety guarantees can evaporate at the boundary. TrustInSoft Analyzer can track data and behavior across these language boundaries, identifying issues that arise from the interaction itself rather than within individual modules. As modern systems increasingly become multilingual patchworks, this ability to analyze the whole system rather than its disconnected parts may prove to be one of the most valuable capabilities of all.
All this brings us back to those ancient libraries and our old friend, the Ship of Theseus (and you thought I couldn’t sail that ship home). We are building modern systems on layers of software that stretch back decades, balancing precariously on foundational code that has been patched, prodded, extended, and occasionally abused, but is now rarely fully understood. For years, we’ve lived with the uneasy assumption that “it seems to work” is good enough, even when we suspect that something is lurking somewhere deep in the stack, quietly biding its time (be afraid, be really afraid).
What’s changed is not just that we now have better tools; it’s that we are starting to demand better answers. “Probably correct” is no longer sufficient when software is steering cars, controlling aircraft, securing communications, and, increasingly, making decisions on our behalf. In this new world, trust isn’t something we can bolt on after the fact; it needs to be engineered in from the start—and, ideally, proven.
This is where TrustInSoft’s approach provides a glimpse of the future. Not just finding bugs but proving their absence. Not just testing what might happen, but mathematically exploring everything that could happen. And now, with AI helping to smooth the path, this level of rigor is no longer reserved for a handful of specialists; it’s becoming something the rest of us can actually use.
Of course, there’s a certain irony here (said Max, ironically). At the very moment AI is helping us write more code, faster than ever before, but oftentimes of questionable quality in terms of bugs and vulnerabilities, we are also turning to equally sophisticated tools to check that code, line by line, path by path, value by value. It’s a bit like having one very enthusiastic apprentice hammering out code at high speed, while another—rather more pedantic—assistant follows along behind, muttering, “Are you sure about that?”
The bottom line is that in a world where software is only getting bigger, older, and more complex, trust is no longer something we can assume—it’s something we need to justify. We may never be able to “prove” trust in the human sense, but with AI-guided formal verification, we can at least prove the absence of entire classes of failures. And that’s a pretty good place to start.
