My last post about Axiom was in late April.
Now, six months later, I've finally reached a milestone I've been working toward: putting Axiom to the test on an external open-source repository for the first time.
What I'm trying to build is not simply another tool that checks AI-generated code.
The ultimate goal of Axiom is to verify formally specified claims and requirements that AI agents autonomously derive from potential contradictions they discover in a codebase.
In other words, an AI agent analyzes a codebase, identifies potential inconsistencies, and formulates its own formal specifications and requirements. Axiom then takes those claims and subjects them to formal verification.
This was the idea I wanted to put to a real-world test.
The target was nim-toml-serialization, an open-source TOML parser written in Nim. TOML is a configuration file format commonly used by software applications.
During the experiment, AI agents analyzed the codebase and proposed several candidate inconsistencies. We selected one, turned it into a formal specification, and ran it through Axiom's verification engine.
The result was interesting.
The parser accepted certain raw control characters inside strings, even though the TOML specification forbids them. Axiom's verification engine found a counterexample showing that the formal claim did not hold.
But the first run also exposed a problem in Axiom itself: a flaw in its verification pipeline prevented the counterexample from being validated against the actual program.
At that point, there were two options: reshape the verification target to obtain a passing result, or acknowledge the problem and fix the verification pipeline.
I chose the latter.
After fixing the pipeline, I ran the experiment again and confirmed that the counterexample was reproduced by the actual parser.
The experience was a useful reminder that verification systems themselves can have defects—and that a trustworthy system must be able to expose its own failures rather than conceal them.
Of course, there is still a mountain of work ahead. This experiment does not establish that Axiom can correctly verify arbitrary codebases against arbitrary specifications.
Nevertheless, I consider this the first real-world prototype demonstration of what Axiom is intended to make possible.
For the first time, I was able to exercise an end-to-end path on an external codebase: AI agents proposed inconsistencies, those findings were expressed as formal claims, a verification engine found a counterexample, and the result was checked against the actual program.
The past six months have been about building the foundations needed to test this idea.
Now, I'm beginning to demonstrate its potential through real code and verifiable evidence.
Top comments (0)