Founding thesis, evidence base and path to scale
Thesis
AI is making software cheaper to produce faster than it is making software trustworthy. The gap matters most where software moves a machine.
I’m building Symbolia in that gap. A customer brings an industrial change. We establish what it must do, check it against those requirements and preserve the evidence as the installation changes. The customer gains a sound basis for putting an improvement into use.
The scale I’m building for is industrial. Manufacturing and heavy industry sit within a broad industrial economy producing roughly $30 trillion of annual value. MM13 I want verified optimisations to create $1 trillion of additional realised annual customer benefit. Symbolia’s 10% share would make that a $100 billion annual opportunity. The ambition rests on making dependable improvement repeatable across machines and factories.
Industrial agents already generate automation code and configure projects. AI-assisted proof systems are advancing alongside them, and external verification has been used on a real safety-critical PLC project. These are the beginnings of a service that combines industrial expertise with increasingly capable machines. IN03 IN04 FV07 FV13
I expect assurance to become part of deployment itself. Generation can be abundant only if dependable use can scale with it.
I. The Next Bottleneck
Writing a program and establishing that its behaviour is acceptable are different kinds of work. The person who wrote it once carried much of the context needed to review it. AI separates those tasks.
Google’s 2026 DORA analysis describes engineers spending time saved in coding on auditing and verification. Faster authorship left more work before reviewers. IN02
Industry is entering the same transition. Siemens’ agents generate automation projects; its work with NVIDIA aims to connect simulation with operational changes. Anthropic’s Model Hardware Standard preview lets models discover and operate programmable equipment through common interfaces. IN03 IN04 IN05 IN06
More of the world is becoming readable by machines, and more of its instructions will come from machines. The scarce step moves towards the person who must authorise the change.
II. Symbolia
Symbolia will make industrial knowledge reusable. We will establish what a machine can be trusted to do, preserve the evidence and carry it into the next compatible installation.
For each controller patch, production sequence or configuration change, the customer receives an account of what has been established and what remains open. Continuous assurance means keeping that account current as the machine changes.
Suppose a controller must wait for a fresh fixture confirmation before starting a tool. A useful check establishes that rule for an exact controller build. Measurements must then establish that the installation’s signals mean what the model assumes. A firmware change may preserve the logic while invalidating a timing assumption.
The evidence must keep those distinctions. A proof, a finite model check, a test and a vendor specification each support different claims. Authors never approve their own work. Unknown effort and cost stay unknown.
III. Why Industry First
A robotic cell already has geometry, states, signals and repeated sequences. Much of its world has been represented for control. That makes industry fertile ground for verification.
IFR reported 4.664 million industrial robots operating in 2024 and roughly 542,000 new installations that year. This is an existing industrial base on which to begin. IN07
My first customers are manufacturers using robotic equipment to make products. They benefit when dependable changes increase useful production, shorten commissioning or prevent disruption. Machine builders and integrators can help us reach related installations.
I’ll begin beside the existing engineering approval process, leaving safety-rated protections in place. Human-written and legacy code supply useful first cases; earlier changes also provide the variation needed to measure reuse.
The initial service will be narrow. Repeated cells in one controller family offer sequences, handshakes, timeouts and restart behaviour we can learn to check well. The first engagement starts smaller: one arm in an investor’s spray-coating business, with the reach-envelope method first to qualify.
Repetition is the experiment.
IV. The Technology Is Arriving
Several parts of verification are becoming easier at once.
AlphaProof demonstrated mathematical search guided by formal feedback. VeruSyn and VeriStruct advanced software-proof construction. SymCrypt connects production-oriented Rust to Lean verification; AXLE provides infrastructure for proof work. FV09 FV07 FV08 FV04 FV11
CERN–GSI brings the precedent closer to our first customer: externally delivered verification found discrepancies in a real safety-critical PLC project. FV13
These advances reduce the work of stating a problem, translating software, finding proofs and maintaining results. I can build a useful service as each part improves. The research chapter records what the demonstrations establish.
V. The Assurance Compiler
I think of the system as a compiler for evidence. It takes code, requirements and knowledge of the installation, then produces an inspectable account of why a change meets its requirements.
The first task is to ask the right question. A program can perfectly satisfy the wrong theorem. Microsoft’s work on intent formalisation addresses precisely this problem. FV16
How fresh must a fixture confirmation be? Which sensor faults matter? What happens after a restart? Which timing bounds have been measured? The engineer approves the meaning before a proof can support release.
The checked model must then describe the actual implementation. Proving a rewritten controller establishes a result about the rewrite; the connection to the deployed program needs its own justification. FV04 FV05
Different questions need different tools: logical solvers, model checking, proof assistants or physical tests. The required architecture separates proposal, checking and approval. Customer agents propose software and deployment designs. Symbolia’s agents formalise requirements and prepare claims and evidence; deterministic checkers judge them against the protected requirements. Neither proposing role can approve its own work or change the acceptance rule. FV01
The resulting package binds the software, equipment versions, assumptions, evidence and approvals. A few human claims expand into their supporting questions. People and customer agents receive the same conclusions and gaps from one read of the validated records. A claim about the whole machine needs an argument connecting its parts.
Then the evidence stays alive. When firmware changes, the engineer can ask: what must we establish again?
VI. The Industrial Assurance Graph
The Industrial Assurance Graph is the world graph at the heart of Symbolia. It connects what we know about components to the conditions, measurements and checks that make the knowledge useful.
Imagine the next workcell arriving with a robot family already modelled, a controller instruction set understood and a scanner’s behaviour characterised. The new installation inherits that work wherever its conditions hold. Engineers concentrate on what is different.
This is where verification begins to behave like compilation.
Each customer’s evidence stays protected. Shared contracts and methods carry explicit permissions and versions. Measurements retain the conditions under which they were taken.
Our advantage will come from justified knowledge that takes contact with industry to acquire: device behaviour, integration faults, accepted engineering practices and the consequences of real changes. Better models will be available to competitors too. Useful reuse and maintenance must make our accumulated knowledge worth more than its cost. MM09 MM10
I’ll test that in two ways. First, measure the second arm against the first. Later, compare the graph with the strongest available model and public tools on unseen changes at matched expert and compute budgets. Separately, record the cost of each library release and what it contributes to deployments withheld from its construction. More mapping must buy useful coverage or less future work.
VII. Timing
The first stage is a closely supported service for a narrow equipment family. The next is a repeatable product whose related deployments require less specialist effort. The second-arm comparison tests that transition.
From there, I intend to check AI-generated changes within agreed operating limits and extend the service across equipment vendors. The destination is assurance infrastructure for automated production.
Expert work can fund reusable knowledge. Better proving models can lower delivery cost. Better coding models can increase the changes customers want to make.
Both curves can favour the same company.
VIII. Competition
Code Metal, TrustInSoft and Axiom already work on verified software. Siemens owns engineering workflows, equipment knowledge and customer relationships. These are capable competitors and potential partners. MM01 MM04 FV10 IN03
I’ll use the strongest proving engines available. Our work belongs in understanding industrial behaviour, connecting evidence across machines and keeping it current. Independence earns its place when customers get something useful across suppliers that a bundled tool does not provide as well.
Each new checking method enters the trusted core and requires a core release. Qualifying one before funding another keeps the cost of broader coverage visible.
The company must know what a change means, what it depends on and what the evidence establishes about it.
IX. Business Model
We will charge for onboarding and formalisation, a fixed fee for maintained assurance, and 10% of agreed, realised benefit from customer-proposed improvements. The fixed fee pays for useful checking, including findings that prevent a bad release. The gain share rewards value delivered in operation.
The economic unit is a consequential change. To scale, we must reduce total effort on comparable work, counting failed evaluations, customer review and maintenance. I’ll measure engineering time, commissioning delay, discrepancies found and the usefulness of the evidence to the release approver.
As checking becomes part of routine deployment, maintained assurance becomes infrastructure.
X. What Must Be True
Four results will earn expansion.
Technical fidelity: the claims describe the actual implementation and configuration.
Customer utility: the evidence improves an engineering decision beyond existing review, testing and simulation.
Compounding economics: related deployments need materially less specialist effort at comparable coverage and quality.
Commercial acceptance: customers pay again and use the evidence in their workflow.
The programme tests deployment reuse and return on graph investment. Internal simulations already show bounded arithmetic reuse and useful failure detection. Adapter experiments have explored further situations, some still awaiting integration. Customer value, physical validity and lower total delivery cost remain the next evidence to earn. The sources record the implementation boundaries. SY01 SY02
XI. The Larger Thesis
I began Age of Wonders with an observation: abundance often arrives before access.
The universe was there before the instrument. The sunlight was there before the grid. Capability can exist before the infrastructure that makes it useful.
Machine intelligence is entering the same transition. Symbolic Superintelligence describes a compilation boundary: human objective, AI cognition, program synthesis, verification and bounded execution. The model proposes; protected rules govern what reaches the world.
I’m building that boundary into Symbolia. My ambition is larger than robotics. As intelligence becomes cheaper, more of the world will be designed and controlled through software. We need a dependable way to decide which instructions can act on it.
That is the AI safety problem I intend Symbolia to solve. Make intelligence safe to put to work.