When the World Runs on Code No One Can Understand: The Future of AI Code Verification and Formal Methods

A Warning from the Mathematics Community

In June 2025, the International Mathematical Union (IMU) endorsed a document known as the Leiden Declaration. Founded in 1920, the IMU is the most authoritative international organization in the global mathematics community, responsible for awarding top honors such as the Fields Medal — its endorsement represents the collective position of the mathematical community. The Leiden Declaration is named after Leiden University in the Netherlands, one of Europe's oldest universities with a deep tradition in mathematics and logic. The declaration was released just as large language models (LLMs) were being widely adopted for mathematical reasoning and code generation. Its core warning strikes at the Achilles' heel of the current AI wave: artificial intelligence is threatening the verifiability of proofs — as AI systems begin participating in the construction of mathematical proofs, the "proof chains" traditionally reviewed step-by-step by human mathematicians may develop untraceable points of failure.

However, a more constructive counter-perspective emerged in the discussions surrounding the declaration — rather than saying AI threatens mathematical rigor, mathematics actually provides the infrastructure to make generative AI more trustworthy. This viewpoint argues that the entire tech industry should treat "mathematical rigor" as a core mission.

Specific pathways include: building public infrastructure for verifiable software, open-source libraries of verified components and specifications, unified standards and benchmarks, better update-checking tools, and interdisciplinary training programs connecting mathematics, computer science, engineering, and national security. The foundation of all of this is sustained investment in the deep mathematical underpinnings of Formal Methods — not just investing in the application layer, but in foundational mathematical research and education.

Formal methods are a set of techniques based on mathematical logic used for precise specification, development, and verification of software and hardware systems. Core tools include theorem provers (such as Coq, Lean, and Isabelle) and model checkers (such as SPIN and TLA+). Take Lean, which has gained the most momentum in recent years — it is both a programming language and an interactive theorem prover, allowing users to write mathematical propositions in a formal language while the machine verifies the correctness of each reasoning step. Lean's math library, Mathlib, has accumulated over a million lines of machine-verified mathematical theorems. Formal methods already have mature applications in safety-critical domains such as aerospace (e.g., NASA's flight control systems), chip design (e.g., Intel's floating-point verification), and railway signaling systems. However, their adoption in general-purpose software development remains very low, primarily due to high usage costs and steep learning curves — which is precisely why the Leiden Declaration calls for increased investment.

"No One Understands the Code" Is Already the Status Quo

In community discussions, many developers offered a calm rebuttal to the panic over "code no one understands." They pointed out: this situation has existed for a long time already.

"Modern codebases routinely contain millions of lines of code, and no one can fully understand them. We just break them into small pieces to deal with."

Today's software systems are built on deep dependency stacks — libraries built on top of other libraries. In the JavaScript ecosystem, for example, a typical Node.js project may have only a few dozen direct dependencies installed via npm, but its transitive dependencies (dependencies of dependencies) often number in the hundreds or even thousands of packages. Some of this code comes from defunct companies, some was written by open-source authors who passed away twenty years ago, mixed in with all sorts of code of uncertain provenance.

This fragility has been demonstrated multiple times: in the 2016 "left-pad incident," a single npm package containing just 11 lines of code was removed by its author, causing build failures across major projects including React and Babel, temporarily paralyzing the entire JavaScript ecosystem. The 2021 Log4Shell vulnerability (CVE-2021-44228) showed that a security flaw in a Java logging library buried deep in the dependency stack could affect billions of devices worldwide. These events vividly confirm a fact: "the world runs on code no one fully understands" has never been a new problem introduced by AI — it is an inevitable result of accumulated software engineering complexity.

Another analogy comes from the compilation process: the high-level languages we write are ultimately compiled into machine code, and virtually no one can directly read that machine code. Yet the entire system still works — because we understand and trust it at the meta level. From this perspective, AI-generated code might simply be yet another link in this ever-growing chain of abstraction layers.

The Critical Difference Between AI-Generated Code and Compilers

However, the analogy of equating AI code with "just another layer of abstraction" was met with a rather persuasive rebuttal from one developer. This is the most thought-provoking technical point of divergence in the entire discussion.

Compilation Is Predictable; AI-Generated Code Is Not

The compilation process is fundamentally predictable and repeatable. It does not make arbitrary autonomous decisions about code — it is simply a relatively direct translation from source code to machine code. The same input always produces the same output.

Modern compilers like GCC and LLVM/Clang follow strict language specifications (such as the ISO/IEC 9899 standard for C), transforming source code into machine code through well-defined stages: lexical analysis, syntactic analysis, semantic analysis, intermediate representation optimization, and target code generation. To further ensure compiler correctness, academia has even developed "verified compilers" — the most famous being the CompCert project, a C compiler formally verified using the Coq theorem prover, capable of mathematically proving that its output machine code faithfully preserves the semantics of the source code. Compiler determinism is one of the cornerstones of the entire software engineering trust chain.

AI is the exact opposite:

"AI often works under vague, poorly designed instructions, and makes a huge number of its own decisions — it may even ignore what you told it and instead implement what it thinks should be done."

Transformer-based large language models (such as GPT-4, Claude, and Codex) compute a probability distribution over all possible next tokens in the vocabulary at each generation step, then select from this distribution using temperature parameters and sampling strategies (such as top-p/nucleus sampling). Higher temperatures produce more random outputs; even with temperature set to 0 for greedy decoding, different prompt phrasings, subtle differences in the context window, or even hardware-level non-determinism in floating-point operations can lead to dramatically different outputs. More critically, these models optimize for the statistical objective of "next token prediction" during training, not the logical objective of "code correctness" — they lack genuine program semantic understanding and merely mimic code patterns from their training data in a statistical sense.

This developer shared a personal experience: when he asked an AI to modify a piece of code, the AI not only completed the requested change but also made other unrequested modifications — changing behavior or quietly introducing subtle bugs. The root cause of this "taking liberties" is that models tend to generate code patterns with the highest probability in the training distribution, rather than making the minimal modifications that strictly follow user instructions.

Non-Determinism Is the Core Risk

This is the crux of the problem. Traditional "code no one understands" is at least deterministic — it can be debugged and traced. What AI introduces is non-determinism and autonomy — it is not a passive translator but an active participant that "takes liberties." This also explains why the Leiden Declaration emphasizes the importance of formal verification: only mathematically provable constraints can put trustworthy reins on an unpredictable generation process.

The Future of AI Code: Will the Panic Subside or Deepen?

Regarding the widespread anxiety triggered by AI code, two starkly different historical perspectives exist within the community.

The Optimists: Growing Pains of Technological Maturity

Some hold an optimistic view rooted in historical cycles:

"AI is the hot topic right now because it's new, powerful, and unreliable. Everything right now is experimental and the future is unpredictable. But history tells us that as systems mature and become familiar, the panic and doomsday declarations will subside. It's like the era when electricity and airplanes first appeared. One day you'll say: I was there."

This view treats AI as yet another typical technological revolution — accompanied by fear and chaos in the early stages, ultimately settling into routine.

The Pessimists: Lost Programming Knowledge and Unchecked Power

Other voices are much darker. Some worry that programming knowledge itself will gradually be lost as visual editors proliferate — just as factory work went from high-paying, high-status positions to being gradually replaced by automation and reduced to minimum-wage jobs, the ICT industry may follow the same trajectory. As more and more people rely on visual tools that "translate into real code," raw coding ability is quietly eroding.

This concern aligns closely with the "deskilling" theory in labor economics. The concept was first systematically articulated by sociologist Harry Braverman in his 1974 work Labor and Monopoly Capital: technological progress tends to decompose complex craftsmanship into simple standardized steps, making work that once required highly specialized knowledge performable by low-skill laborers. In the software industry, this trend is already visible — from assembly to high-level languages, from hand-written SQL to ORM frameworks, from manual deployment to one-click CI/CD, each layer of abstraction lowers the barrier to entry while distancing developers further from the underlying mechanics. The rise of low-code/no-code platforms (such as Salesforce and OutSystems) pushes this trend to its extreme. AI code generation may represent the most radical step on this deskilling chain: when natural language becomes the primary programming interface, the need to understand program execution semantics may decline precipitously.

An even more extreme scenario imagines that in the distant future, programming might be seen as dangerous "sorcery" due to its "power to change everything" and be legislatively banned — because in a cyber world highly dependent on networks and even brain-computer interfaces, those who master code would wield excessively concentrated power.

And the most unsettling line comes at the end of the discussion:

"Or worse: what happens when the last human who tried to understand what the machines built dies of old age, and no one can read it anymore?"

Conclusion: Mathematics as the Foundation of Trust

This discussion started from a mathematical declaration and ultimately touched on a question far beyond technology itself: In a world of systems we increasingly cannot fully understand, how do we maintain trust?

The answer probably does not lie in requiring everyone to read every line of code — that was never achievable. The real way forward, as the discussions surrounding the Leiden Declaration suggest, is to build verifiable infrastructure: using formal methods and mathematical proofs to provide trustworthy boundaries for unpredictable AI outputs.

We don't need to understand every detail of the code, but we need to be able to prove that it won't do things we don't want it to do. When the world runs on code no one can understand, the only thing that might save us may not be more understanding, but more rigorous verification. This is precisely the historic moment when formal methods transition from a niche academic field to an industrial necessity — from the flourishing of the Lean math library, to AWS using TLA+ to verify distributed system designs, to Microsoft integrating formal verification into Windows kernel development, all signs indicate that "mathematics as the foundation of trust" is moving from concept to reality.