Safi Shamsi spent years tracking AI-powered misinformation. Now he argues that as machines write more of the world’s software, mathematical proof—not human review—has become the only scalable way to trust code.
Before Safi Shamsi built the tool that made his name, his job was to catch machines, and the people who use them, in the act of lying. In a previous role, he worked on narrative intelligence, tracing how coordinated networks of bots and influencers push a story across social media until it looks organic. What stayed with him had less to do with the machines being wrong than with the confidence they carried while they did it. He would see the same thing later in his own systems, a model reaching into a corpus and pulling back fuzzy, plausible matches it was never meant to retrieve. “The model doesn’t just get things wrong,” he says. “It gets them wrong confidently, with sources that don’t exist.”
That failure mode does not stay in one domain. The same fluency that lets a model invent a citation lets it write a function that looks correct and is not, and machines now write a great deal of the world’s code. Somewhere in the software running a bank, a hospital, or the phone in your pocket, there is a routine no human wrote and no human fully read: produced by an assistant, skimmed by a developer, shipped. Shamsi argues that the industry has not reckoned with what it means to trust code that arrived faster than anyone could check it, and that the answer is proof rather than another pass of human review. An engineer whose output an assistant has multiplied tenfold cannot read ten times as carefully. The volume has already outrun the old habit of skimming a diff and trusting it.
His fix traces back to his research. Shamsi’s master’s thesis at the University of Birmingham, where he took a data-science degree in 2025, paired knowledge graphs with the vector search most systems lean on and cut fabricated answers by 67 percent, turning what remained into something a person could check. He carried the same method into medicine, publishing at the MICAD conference on using knowledge graphs to classify mycetoma, a neglected tropical disease that has to be sorted into fungal or bacterial forms before anyone can treat it, a call that is slow to make and, made late, can cost a limb. The graph held the record of past cases, so a clinician could see what similar patients had turned out to have rather than trusting a black box. The same instinct runs through Graphify, which answers a question with a file and a line number instead of a paragraph of confident prose, and through Penpax, the Rust engine he is now building for enterprises, which puts formal verification, the mathematical proving of a program’s properties, at its center.
He is not alone in the conviction, and the company he keeps is serious. Martin Kleppmann, the Cambridge researcher whose textbook sits on a generation of engineers’ desks, predicted late in 2025 that AI would drag formal verification into the mainstream. Leonardo de Moura, who created the Lean proof assistant that working mathematicians rely on, put the stakes as a question: when AI writes the world’s software, who verifies it? Fully proven systems already exist, among them a secure operating-system kernel called seL4 and a verified C compiler called CompCert, and startups such as Harmonic are teaching machines to write formal proofs. The problem Shamsi wants to sell into is one the largest labs are circling too.
The blunt version of the critique against tools like his is that memory is just extra steps, text shoved back into a model’s context, burning attention without making the model any smarter. The complaint is not idle. A context window is finite, and every token spent on retrieved text is one the model cannot spend on the problem in front of it. Shamsi grants the shape of it and points to what the enterprise layer does differently: it learns. Over time, he says, it builds a picture of how a given developer works and adapts, so the system sharpens with use rather than simply growing larger.
His case for urgency is plainer than the debate around it. If the foundation of a company is code an AI wrote, he argues, you have to verify it, and you have to index it, because the day something breaks in production you will need to find what went wrong, fast. AI writes long, and length without structure is a liability. It is the same argument, turned toward safety, that makes Graphify useful in the first place. He set the whole thesis down in a book, The Memory Layer, written to gather years of knowledge-graph research in one place.
What gives the case weight is that he marks its edges. On a small codebase, he admits, Graphify barely helps, and he agrees with the developers who tell him so. The payoff shows up on large repositories, where reading every file is the expensive option. He would rather concede a limit than oversell past it, which is the reflex of someone who spent his early career watching confident systems be wrong.
The pattern Shamsi first saw in disinformation is arriving now in code, at a scale that dwarfs it, and the checking is still mostly left to chance. He is a knowledge-graph researcher who does not take a machine’s answer without a receipt, and he has spent his short career building the receipts. In a field slowly learning that it cannot take its own tools at their word, that may be the most useful instinct going.
