Research cut: 7 September 2026. These are the publications and revisions behind my argument. Each entry preserves the claim’s scope; company reports remain company reports. The strategy and illustrative models are my own, with customer validation ahead.
The research chapter develops the argument. This library lets readers examine its foundations; the local dossier retains source manifests and manuscript digests.
Primary source library
Living documentation was inspected on 7 September 2026. Duplicate citations to the same release are identified below.
Industrial demand and deployment
IN01 · Announcing the 2025 DORA Report: State of AI-Assisted Software Development
2025-09-23.
DORA reports widespread AI use and associations with software delivery throughput and stability. The research is observational and self-reported.
IN02 · Balancing AI tensions: Moving from AI adoption to effective SDLC use
2026-03-10.
A qualitative analysis of 1,110 Google-engineer responses collected in Q3 2025 describes creation gains alongside review and audit burdens. Possible survey priming limits interpretation; industrial defect and release rates were not measured.
IN03 · Siemens brings AI to the physical world with Eigen Engineering Agent
2026-04-20.
Siemens announced commercial automation-engineering agents and pilots across more than 100 companies in 19 countries. Productivity and quality figures are company-reported; the assigned-task benchmarks are unspecified.
IN04 · Siemens takes AI for the physical world to the next level with two new Eigen Engineering Agent capabilities
2026-06-17.
Siemens added ECAD integration and project generation. “Standards-compliant” refers to its Automation Framework for project organisation, rather than functional-safety certification.
IN05 · Siemens and NVIDIA Expand Partnership to Build the Industrial AI Operating System
2026-01-06.
The partners outline an industrial AI roadmap linking simulation to proposed operational changes. Autonomous-factory operation remains an ambition.
IN06 · Previewing the Model Hardware Standard
2026-08-27.
A research preview proposes model-agnostic orchestration of programmable equipment, with early partner examples and device-level limits. It is an interface proposal; whole-cell safety requires a wider argument.
IN07 · World Robotics 2025 — Industrial Robots: Executive Summary
2025-09-25.
IFR reports 542,076 industrial robot installations and computed operational stock of 4,663,698 in 2024. These count robots, not workcells or prospective assurance customers. Publication day is corroborated by IFR's report-2025 page.
Relevant location: PDF pp. 3–4 (printed pp. 13–14).
IN08 · The True Cost of Downtime 2024
Published 2024.
Estimated Fortune Global 500 downtime costs extrapolate from 181 online interviews conducted April 2019–March 2023. They describe historical exposure; attributing it to AI-generated changes needs separate evidence.
Relevant location: PDF pp. 2–3 and 14; dated by the report's 2024 copyright.
IN09 · Regulation (EU) 2023/1230 on machinery — consolidated 27 July 2026
2026-07-27.
Articles 3(16), 18, 25 and 54 govern substantial modification, conformity routes and general application from 20 January 2027. Article 18 excludes non-professional modification for own use. The regulation has no universal external-verifier or formal-proof mandate. This consolidated text is documentary; the authentic Official Journal controls.
Relevant location: Articles 3(16), 10, 18, 25, 54; Annex I A(5)–(6); Annex III 1.1.9 and 1.2.1.
IN10 · Regulation (EU) 2026/1744 — Digital Omnibus on AI
2026-07-24.
The act amends the AI Act and machinery framework, including product-AI timing. Its high-risk categories have defined scopes, and future delegated acts remain distinct from completed rules.
Relevant location: Adopted 8 July 2026; Official Journal, 24 July 2026; Article 1(40)–(41), Article 3.
IN11 · We are Changing our Developer Productivity Experiment Design
2026-02-24.
METR explains how changing tools, selective participation and task choice complicate productivity measurement among open-source developers. Its early-2025 slowdown result cannot simply be carried forward to current tools.
IN12 · Measuring the Self-Reported Impact of Early-2026 AI on Technical Worker Productivity
2026-05-11.
A convenience sample reports perceived technical-worker value gains. Very low email response, selection effects and response inconsistencies limit interpretation; the survey measures self-reported value rather than observed speed.
Formal methods and proof infrastructure
FV01 · Validating a Lean Proof — Lean Language Reference
Undated living documentation; inspected 2026-09-07.
Procedures for inspecting assumptions and checking a proof against a protected statement. Trust still depends on the statement’s meaning, checking infrastructure and logic.
FV02 · Elaboration and Compilation — Lean Language Reference
Undated living documentation; inspected 2026-09-07.
Lean's kernel checks core logical terms; a separate compiler transforms intermediate representations to C and native code. Executable unsafe code has a different trust boundary from kernel-checked logical terms. Theorems about logical functions need further justification to support claims about compiled execution.
FV03 · How We Built Cedar: A Verification-Guided Approach
Accepted 2024-04-18; FSE Companion event 2024-07-15 to 2024-07-19.
Cedar combines proofs of Lean models with differential random testing against production Rust. The authors report four validator bugs found through proofs and 21 additional bugs through differential/property testing. The implementation bridge is testing, with reported generator-coverage and untested-API gaps, rather than a proof of whole-program equivalence.
FV04 · Verifying Rust cryptography in SymCrypt, from standards to code
2026-07-13.
Microsoft released proofs for Rust ML-KEM and SHA3 used in Windows Insider builds. Agents assist specification and proof work; maintained extraction and replay connect evidence to code. Low-level boundaries include reviewed models. Broader rollout remains ongoing, and AI labour savings are unquantified.
FV05 · Aeneas — verification toolchain for Rust programs
Undated living repository README; inspected 2026-09-07.
Aeneas uses Charon and Rust MIR-derived representations to generate functional models for proof assistants, including Lean. Its documented translation and borrow-checking work covers a subset of safe Rust. Unsafe code and concurrency support remain in development; some loop/reference patterns are unsupported, and external definitions may need handwritten models.
FV06 · Verus overview — Verus Tutorial and Reference
Undated living documentation; inspected 2026-09-07.
Verus statically checks supported Rust against specifications through verification conditions and SMT solving, without introducing runtime checks. Its trusted base includes the verifier and Rust/LLVM compilers. Language and library coverage is partial; the checking chain differs from replayable Lean proof terms.
FV07 · Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set
First submitted 2026-02-04; inspected revision v3 2026-05-09.
VeruSyn reports 6.9 million synthetic Verus-verified Rust programs used to fine-tune Qwen2.5-Coder-32B. Accuracy@100 with five debugging rounds is 49% on system proof tasks versus Sonnet 4.5's 54%, at about 2% of its inference cost. These benchmark costs depend on sampling and pricing; they exclude the wider assurance process. Validation rejects changed specifications, extra assumptions and nontermination.
FV08 · VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus
First submitted 2025-10-28; inspected revision v4 2026-03-03.
VeriStruct reports success on 10 of 11 Rust data-structure modules and 128 of 129 functions through structured generation and repair of abstractions, specifications and proofs. The evaluation uses curated/modified modules, includes test functions in the count and requires a comprehensive user-supplied test suite. Success is measured against the resulting contracts.
FV09 · Olympiad-level formal mathematical reasoning with reinforcement learning
Online publication 2025-11-12; version of record 2026-03-13; issue 2026-03-19; IMO event studied July 2024.
AlphaProof solved three non-geometry IMO 2024 problems through reinforcement learning and test-time adaptation. Combined with AlphaGeometry 2, the system scored 28/42, within the silver-medal range. Experts formalised the problems; each AlphaProof solution took two to three days of test-time reinforcement learning. Two combinatorics problems remained unsolved. The demonstrated task is mathematical proof search.
FV10 · Releasing AXLE
2026-03-05.
Axiom released the Axiom Lean Engine: infrastructure for Lean proof verification and manipulation. Its technical scope is detailed in FV11.
FV11 · AXLE: A Cloud Infrastructure for Lean 4 Theorem Proving Utilities
Submitted 2026-06-24; accepted at AI for Math Workshop, ICML 2026.
AXLE describes 14 Lean tools, multi-version hosted execution and checks on signatures, axioms and incomplete proofs; authors report over 500 million requests. The paper prioritises cooperating clients and recommends stronger independent validation for hostile submissions. Fixed environments constrain multi-file projects. The count measures infrastructure requests at this revision.
FV12 · Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification
ICLR 2026 proceedings; precise publication day not displayed; supersedes inspected 2025-09-27 preprint results.
Final DafnyCOMP contains 400 programs: 300 chains and 100 DAGs. Main chain evaluation averages 0.55% verification at Pass@8, best 2%; a three-turn verifier-assisted protocol reaches 9.67% for two models. Tasks contain two to five acyclic functions. The eleven model configurations predate this dossier; Claude is excluded from evaluation because it helped synthesise the tasks.
FV13 · Formal Verification of PLCs as a Service: A CERN-GSI Safety-Critical Case Study (extended version)
Submitted 2025-02-26; extended version of NFM 2025 paper.
CERN verified GSI's FAIR Personnel Access System PLC project through separate requirements, development and verification teams. Iteration repaired discrepancies and added reusable models for protected Siemens functions, including timed functions. Those models were checked against documentation and simulated scenarios; hidden implementations remained outside the equivalence claim. The paper reports verifier bugs and leaves commercial cost and AI contribution unquantified.
FV14 · A Verification Framework for Runtime Assurance of Autonomous UAS
DASC 2024, September–October 2024 (author publication list); author-hosted draft.
NASA authors formalise Simplex runtime assurance in PVS/Plaidypvs for three UAS examples. The advanced controller is treated as a black box; proofs concern recovery and monitor sampling. Safety depends on timely detection and a suitable trusted recovery controller under the model's assumptions. More complex composition remains future work.
FV15 · Runtime Assurance of Aeronautical Products: Preliminary Recommendations
January 2023 (report cover; NTRS metadata says 2023-01-01).
NASA's preliminary civil-aviation guidance recommends domain-validated monitor requirements, traceability, evidence linking executable monitors to specifications, verified safe fallback, input assurance and common-cause failure management. Runtime assurance can introduce hazards and needs its own assurance argument.
FV16 · Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents
Shuvendu K. Lahiri · Microsoft Research · 17 March 2026, arXiv v1.
A research agenda for translating informal intent into validated, checkable specifications. The paper surveys early approaches; specification validation and production scaling remain open challenges.
Competition and accumulated advantage
MM01 · Code Metal Closes $125M Series B
2026-02-19.
Code Metal announces a $125 million Series B for verified code translation and hardware optimisation in mission-critical industries. Financing and product direction are company-reported.
MM02 · Siemens launches the Eigen Engineering Agent, bringing purpose-built AI to industrial automation engineering
2026-04-20.
Siemens announces general availability, TIA Portal integration, project-context engineering and output validation. Customer counts and productivity are company-reported. The validation description specifies no formal-proof guarantee or whole-system safety certification.
MM03 · TIA Portal Test Suite V20: Application test — Introduction
2024-11.
Version-pinned documentation for S7-1500 block tests using PLCSIM Advanced, assignments, cycle/time execution and assertions. It describes simulation-based testing.
MM04 · TrustInSoft Announces April 2026 Release of TrustInSoft Analyzer with AI Powered Verification Enhancements
2026-04-28.
The release adds AI-generated drivers/stubs, formal-methods-based MC/DC analysis and integrated Rust workflows. Its body dates the release to April 2026; the official listing supplies day 28. The separate 10 March announcement previews availability. Performance claims remain vendor-reported.
MM05 · Certora Technology White Paper
2025-02-24.
Describes smart-contract bytecode verification against CVL/CVLR specifications, including mutation checks for specification weaknesses. Results concern the supplied contracts under the tool's modelling assumptions.
MM06 · Runtime Verification: Our Work
Undated living documentation; inspected 7 September 2026.
Describes formal verification, modelling, fuzzing, design review, reusable customer artifacts and embedded-systems assurance. Service scope and customer outcomes are supplier-reported.
MM07 · Aristotle Learns to Code, Achieving New State-of-the-Art of 96.8% on Code Verification Benchmark
2025-12-03.
Harmonic reports 160 proofs and 23 disproofs among 189 supplied VERINA algorithm/specification tasks. The 96.8% figure concerns this benchmark with given specifications.
MM08 · Releasing AXLE
2026-03-05.
Duplicate of the primary release catalogued as FV10.
MM09 · Dierickx and Cool: Asset Stock Accumulation and Sustainability of Competitive Advantage
1989-12-01.
The publication's abstract identifies asset accumulation, imitation, substitution and mechanisms including time compression, complements and erosion. Inspection covered publisher metadata and abstract; the detailed argument was read in the authors' working paper MM10.
MM10 · Dierickx and Cool: Asset Stock Accumulation and Sustainability of Competitive Advantage — INSEAD working paper 87/46
1987-12.
The authors explain time-compression diseconomies, complementary stocks, erosion and substitution, stressing that these properties vary between accumulation processes. This March 1987 draft was revised in December, before the 1989 final publication. Its application to Symbolia is my analysis.
MM11 · The Lean Language Reference: Introduction
Undated; inspected 7 September 2026.
Lean uses a small independently implementable proof-checking kernel, with independent implementations available. The manual described version 4.34.0-rc2 on access. Construction and checking are separate; checking cost still depends on the proof.
MM12 · Clay Mathematics Institute: P vs NP
Undated; inspected 7 September 2026.
P versus NP remains unsolved. This is complexity background, not a lower bound for Symbolia’s tasks or graph. A large brute-force search space leaves better algorithms possible.
MM13 · World Bank: Industry, including construction, value added (current US$)
World, 2024; World Development Indicators update 13 July 2026, retrieved 13 September 2026.
The World Bank API returned $28,403,795,045,949.50: roughly $30 trillion in annual industrial value added. The industry definition covers manufacturing, mining, construction, electricity, water and gas. Value added deducts intermediate consumption; it is not gross sales or an assurance budget. The retained response fixes the edition used here.
This is the economic scale behind my target in manufacturing and heavy industry. The $1 trillion annual improvement ambition is my thesis. At a 10% share of that agreed, realised benefit flowing through Symbolia, the annual success-fee opportunity is $100 billion, before fixed fees. The calculation describes the scale I intend to pursue.
The manuscript lineage
The origins chapter follows the current Age of Wonders manuscripts and my account of the walk. SHA-256 digests identify the versions read; the named PDF editions were not compared page by page. Irreducible remains a published historical predecessor to Symbolic Superintelligence.
- Create An Age Of Wonders — canonical essay.
- Perceptual Abundance — canonical essay.
- Its All Energy — canonical essay.
- Computational Abundance — canonical essay.
- Bridge To Infinity — canonical essay.
- The Free Starship — canonical essay.
- Symbolic Superintelligence — canonical essay.
- Irreducible — historical predecessor.
- Love Is The Foundation — canonical essay.
Internal prototype evidence
SY01 · Symbolia’s simulated energy-network engagement and architecture reconciliation
Private development record, independently re-read within the project on 12 September 2026. This is my prototype evidence; customer validation and public replication remain separate.
The transfer registered fifteen obligations, checked three existing arithmetic certificates and kept twelve gaps open. A repeat reused the three certificates without new worker execution. Fifteen exact scalar fields and fifteen preview identities reproduced. Later reviews retained failures and corrections in preparation, output bindings and applicability. The private evidence manifest identifies the receipts.
These records show bounded method/cache reuse and useful failure detection. Total labour savings, production isolation, physical validity and return on graph investment remain unestablished. The programme will test reuse at equal coverage and recorded cost. External sources retain their original inspection dates.
Historical checkpoint, 13 September 2026. The accepted core then carried 1,046 passing tests; SY01’s claims were unchanged. At that checkpoint, four qualifications awaited independent acceptance: the public path, world-graph reuse, world-graph investment, and reuse on a second deployment. The public path had local test results; the two world-graph qualifications were unstarted. Physical validity, labour savings and production isolation remain unestablished. Pending acceptance, unrun tests and failed tests retain distinct meanings.
SY02 · Study-side adaptation examples
Private development record, 12 September 2026. My prototype evidence, awaiting external validation.
In the same energy-network study, I asked whether a new situation fits the architecture, needs a study-side adapter or requires a core change. Each class needed one of those three verdicts.
Study-side adapters exercised screening, premise-domain and pricing examples without editing the retained core. The records name existing arithmetic, return-profile and execution primitives, but some results remained proposals outside the governed claim tree. The thermal-blooming screen did not exercise core integration; the sizing-economics proposal had no registered governed leaf, qualified return-refresh bridge or independently admitted correction. A missing primitive remained an explicit finding. These records support bounded adapter work, not four independently integrated situation classes.
No labour saving, physical validation, hardware feasibility or physical applicability is established. The optical calculations report sampled optical quantities; their fine-minus-coarse quadrature differences do not enclose continuous numerical error or establish electrical output. The economic outputs are symbolic inequalities in unknowns with no actual intercepts: conditional boundaries rather than accounting returns, quotes or physical conclusions. The unfinished return-cycle bridge remains a separate gap. Nothing here concerns robots.
These examples locate useful adapters and unfinished integration. Governed transfer and its cost need separate measurement.
SY03 · Retained public robot-arm datasheets
Retained during September 2026 under the platform plan's arm-data directory. Public vendor documents, republished nowhere.
Manufacturer specifications, stopping-distance data, functional-safety notes and instruction manuals for common industrial arm variants across ABB, FANUC, KUKA, Universal Robots, Yaskawa and Kawasaki, together with lab prototype arms including the Franka FR3, Kinova Gen3, Dobot CR series and uFactory xArm. Several of the retained Kawasaki and Yaskawa documents cover explosion-proof painting robots, which is the hazard class of the first engagement.
These figures enter the claim tree as declared premises with their source, digest and vendor conditions. They remain unmeasured on the installation. A datasheet premise supplies no physical validation.
An independently reviewed recovery organised the figures against fifteen proposed deployment obligations, all open. Exact source-field qualification remains pending; recovered positive votes alone do not confirm the premises.
Current implementation boundaries
The latest local successor has passed its full test suite and independent reviews for internal admitted arithmetic, guarded paired JSON/human reading and independent approval of authenticated proposal registrants. That bounded successor is adopted and open for private pull-request review. These controls run on a trusted local host; they do not recover the original authors of imported source material. Full source-author coverage, public mutation routes, production runtime and physical or customer validation remain open.
Change tracking identifies affected artifacts. Linking each change to the obligations it invalidates remains core work; until qualified, a patch re-checks everything in scope. Reuse experiments must count that work and its maintenance.