I want to say a few words here about the unfolding cybersecurity nightmare and how I think the world can survive it and avoid it turning into a full-on cyber-apocalypse.

The “nightmare/apocalypse” here is basically the following situation: Almost all software has lots of bugs of varying degrees of severity, but it’s historically been very expensive (in terms of compute time and human expertise) to find them. The latest generation of LLMs have now made it much easier, so now almost everyone can be hacked in one way, and another, and another, and another…

These issues have been all over the news recently due to a spate of “rogue AI” attacks from AI agents at OpenAI, Anthropic and Google… which turned out to be most centrally due to a misconfiguration in the software they were all using to run their security tests, which was made by an Israeli company called (wait for it) Irregular. If you made this stuff up, nobody would believe it!

“Apocalypse” is a dramatic term—but it’s also evocative of the severity of what’s at stake here. This doesn’t have to be a globally epically tragic situation, but to avoid it becoming that, a lot needs to be done.

Unsurprisingly, I don’t think that pausing or unplugging AI is the answer. Theoretically, it could be the answer if done globally—but aside from the costs we would incur from losing all the good AI is doing and will do as it develops, and the ethical and practical downsides of imposing a global anti-AI fascist order… this simply isn’t realistic. The major global powers are now all hacking each other using AI, as are various minor powers, and even if they all promise to stop developing and using better hacking models none of them are going to. So the solution has to be something different.

Careful shoring up of critical bits of infrastructure using state-of-the-art security is part of the immediate answer. Effective leveraging of AI cybersecurity tools to combat the AI hacking tools is also part of it. My main point here, though, is that the crux of the answer has got to be more fundamental—basically, to leverage AI coding and theorem-proving agents to replace (step by step) all the buggy code in the world with formally-verifiable, correct-by-construction code. It’s a big job but with AI agents we can do it, and at the end we will all be way better off. Most of the tooling needed is already here, and many of us are hard at work finalizing the rest of it.

The shape of how to make this fundamental solution work is the crux of what I’ll talk about in this post. First, though, I want to share some specific recent experiences that have made these cybersecurity issues top of mind for me—and that I will use as a running example through the rest of the post.

SingularityNET’s Recent Hack Experience

Absurdist big-tech theater aside, the AI cybersecurity apocalypse has become a very vivid and massively upsetting issue for me over the last couple weeks—because SingularityNET, my AI-plus-blockchain project, got hacked, and in a significant way.

We haven’t worked through all the forensic details yet, and nobody should take this blog post as a definitive source of truth on this recent hacking event… but roughly speaking, what it looks like now is: over $2 million USD worth of tokens across several chains was stolen by hackers from a token bridge. A “bridge” being the piece of infrastructure that lets tokens move from one blockchain to another, which is exactly the kind of place where a lot of value sits behind a relatively small amount of code.[2] What is looks like right now is: The hack maybe wasn’t centrally a blockchain thing at all… rather, at the core seems to have been a hack of some code related to our use of Amazon Web Services. As best I can tell so far, there was some old AWS infrastructure set up by some of SNET team members around 2018, and it looks like a bunch of LLM agents were used to find a bunch of small vulnerabilities in it and put the pieces together to get into a secured part of our AWS setup, which yielded keys that allowed tokens to be minted in the bridge.

I’m not a security professional myself, so I won’t try to go through all the technical particulars of what happened. We have some fantastic security pros under contract, and they’re digging into all of this. Meanwhile we have rebuilt the relevant pieces of the infrastructure, so that the key parts needed to perform this sort of function are now done in the most modern and secure way we know how.

Around $1.5M USD of the tokens involved in the hack were AGIX (our legacy token before we merged into the ASI Alliance). However for SingularityNET community members reading this, I should say clearly that: Our treasury tokens, and the tokens of ordinary holders, were not affected. This was a hack of a bridge, and the minting functionality in a bridge is secured differently from the multi-signature wallets we use for the treasury, and differently again from tokens simply sitting on a public blockchain.

A couple of days after this hack was discovered, I saw that one of the big exchanges (BitGet) had (in a separate, unrelated incident) been hacked for something like $387 million.

A good friend of mine who hacks for a living has found an endless number of deep security flaws in the infrastructure of big companies—collecting bug bounties along the way—and recently found a nasty one in WordPress, which the majority of websites on the web run on. More and more bugs are being found, faster and faster…

This is the shape of the potential cybersecurity apocalypse. It isn’t one dramatic day when every computer on Earth stops working. It’s a shift in the economics of attack: nearly all the software running the world was written under the tacit assumption that finding its weaknesses takes scarce, expensive human attention, and that assumption is now colliding with adversaries who can throw cheap, tireless machine intelligence at the problem in parallel. The models don’t have to be infallible. They don’t have to be AGIs. They just have to make enough previously-uneconomical attacks worth attempting, and the numbers do the rest.

So what do we do?

Fortunately the shape of the solution is as clear as the shape of the problem. After needed short-term stopgap remedies are put into place (easy to say but not at all trivial in practice), the actual medium-terms solid solution to this cybersecurity problem is basically “In Math We Trust.”

That is: We have to make the entire software stack formally verifiable, from the English-language statement of what a system is supposed to do, down through the specification, the contracts and application code, the language runtime, the operating system and the microkernel, to the assumptions about the hardware—with each layer stating what it guarantees and connecting to the layers above and below it, so that no layer capable of defeating a security claim disappears into unspecified glue code or whatever.

The following table unfolds this story in a systematic way—which is a little bit technical, but that’s the nature of the beast. The rest of the post walks through these layers.

First, to reiterate the boring-yet-important part

Obviously, knowing the medium-term path to solving the cybersecurity apocalypse doesn’t exempt everyone managing deployed software systems (including me as SingularityNET CEO) from making the shorter-term patches and improvements we need in order to avoid further near-term hacks. I feel quite bad that we didn’t put more time into shoring up our old AWS infrastructure code against the sort of attack we experienced—which, of course, nobody envisioned when that infrastructure was set up in the previous decade. We have a great team doing that re-implementation now, and from the immediate-term perspective it’s the most important thing happening at SNET on the security front. If there’s a lesson here for everyone else, it’s that your 2018 or 2008 code is being read, right now, by countless swarms of adversarial agents that don’t get bored.

However, we also need to think about how to make sure bigger and bigger incidents of this sort don’t just keep occurring, over and over and over again, to everybody—which has a few different layers in itself…

Fight AI with AI: Omega Purple

One partial solution my colleagues at SingularityNET and BGI Labs are working on now, and hope to roll out early next year, is the obvious one: use AI to find the bugs and fix them. You can talk about red-team AI, which tries to find bugs—and every company should be doing more of this, using LLM-based agents to attack their own software infrastructure; if we had consistently spent more time and money on that at SNET, we would not have been hacked. And there’s blue-team AI, which goes in and secures things in the smartest way it can.

The framework I’ve been prototyping for this, called Omega Purple, uses our own neural-symbolic Omega agents for the red team, other Omega agents for the blue team, and a third, independent role that reconciles what the two sides claim. In the design we call them Redbot, Bluebot and Purplebot. Redbot works out plausible attack paths and proposes authorized tests; Bluebot asks what should have prevented or detected each of those actions, then goes and checks the actual controls and telemetry; Purplebot makes sure neither side grades its own homework, because a missing alert is not proof that an attack was blocked, and a plausible-looking patch is not a closed incident.[3]

The thing that makes this more than three chatbots arguing is that they all share an AtomSpace: a symbolic model of the network they’re attacking and protecting. The main asset is really that world model. It ties software revisions to the actual deployments, to the identities and permissions that can reach them, to the business services they support and the controls around them—so a suspicious code path gets judged by whether it’s deployed, who can get to it and what authority it leads to, not only by how ugly it looks in the repository. Repository-level vulnerability analysis (including e.g. Visa’s open-source Vulnerability Agentic Harness, which I’ve been experimening with) feeds into that wider picture rather than replacing it.[3]

You can’t play whack-a-mole forever

Products like Omega Purple will be necessary. On the other hand, we don’t want to rely on playing whack-a-mole with bugs forever. That is not, in the end, a robust approach. The find-and-fix loop lives inside whatever architecture it inherits, and if the architecture lets a compromised service reach a powerful key, or slip past an approval check, then the defenders are condemned to keep discovering and blocking those routes one at a time, indefinitely, against an adversary that never sleeps.

So the first thing we’re doing in that regard is giving Omega Purple an additional capability: look at a software system, find the most critical functions in it, and replace the code underlying those functions with software that is provably correct by construction—and provably can’t leak.

There’s a robust body of knowledge on writing provably correct software. If you have a formal spec of what the software is supposed to do, and code that tries to do that thing, and the code is written in a reasonable programming language—MeTTa, say, or even Rust; C with a lot of pointers doesn’t work too well, but anything that isn’t too mired in the machine architecture and is reasonably high-level will do—then you can use mathematical theorem provers to prove that the program actually does what the specification says. Formal verification changes the question being asked. Testing and scanning ask “have we found a bad execution?” Verification says: here is a property, stated precisely; here is a machine-checked argument that it holds for every execution covered by the model and its assumptions. What you get is not a certificate stamped SECURE, so much as a checkable explanation of exactly which bad thing cannot happen, and why.

Take the part of a bridge contract that mints new tokens, or the signing service that authorizes a transfer out of a bridge or a custody application—the exact kind of functionality that was abused in the hack against us, and the place where value finally gets released. You could require that every signature bind one exact transaction: destination, amount, tenant, approval quorum, policy version. Revoked approvers must not count. A replayed authorization must not produce a second transfer. And if the authorization state is uncertain, the service must refuse rather than make a convenient guess.[3]

There is a lot of subtlety here that people tend to miss. Proving the decision function correct is only half the job, and it’s the easier half. If a legacy administrator endpoint can sign directly, or some cloud service can extract the key, the attacker simply walks around the theorem. In the case of our own hack, doing this right would have meant putting the AWS pieces and the smart-contract pieces all inside the boundary being formally validated—which would have required carving the critical bits of code out from the rest of our AWS code. That is obviously the right thing to do anyway. And emergency access, upgrade paths and recovery procedures have to be inside the boundary too; that’s where the invisible exceptions live.[3]

Getting down to the software architecture level—“object capabilities” are the natural architecture for making this all work. A capability is a protected, unforgeable reference that grants some specific authority over some specific thing—a key that opens one door, rather than a badge that says “trust me” at every door. You give a worker access to one bounded operation, not ambient access to the whole machine plus an instruction to behave. The authority lives in an enforced connection, not in a reassuring sentence in a prompt or a field labelled “permission” in a JSON document.[4] Picture a bridge frontend that has been completely compromised: it can still submit a transfer proposal, because that’s its job, but it cannot obtain a signing key, manufacture an approval or replace the policy service. The security objective is no longer “our AI will recognize every malicious request.” It is that even a thoroughly hostile frontend can’t cause the protected effect without satisfying independently enforced conditions. I’m not claiming that a system we hadn’t built would certainly have stopped what hit us—only that this is the shape of what would have made it far harder.

The spec is the hard part

This is all very elegant in principle and on the math level, but then when you try to apply this to general-purpose software, you hit the problem that specifications mostly don’t exist – we don’t have a precise specification of what most general-purpose software is supposed to do. A theorem prover will happily prove the wrong specification perfectly. If “only authorized users may transfer funds” is the whole requirement, none of the hard questions have been answered: authorized when? for which account? under which policy version? what happens when an approval is revoked between submission and execution? And faster code generation makes this worse, not better. A model picks a plausible interpretation, writes code implementing it, then writes tests that congratulate the same interpretation—and asking a second model to review doesn’t necessarily help if it shares the first one’s assumptions, which models trained on the same internet tend to. The scarce resource stops being code and becomes justified trust.[9]

Again, AI agents can help. I’m working with a hive of Omega agents that tries to make a formal spec for an informally specified bit of software and iterates with humans to get the spec just right. The specification side of this, in my current working prototype, is what I’ve been calling Plain2MeTTa: Plain is a constrained, English-readable specification language, structured enough for machines to process but readable by the person who is actually responsible for what the system is supposed to do, and the pipeline links the exact source text to its interpretations, typed contracts, implementations and separately attributed validation evidence, so that when something changes upstream the dependent artifacts are invalidated rather than letting yesterday’s assurance decorate today’s code.[9]

The interpretation hive takes the hardest step—turning readable requirements into precise meaning—and organizes it adversarially. Several agents from different model families interpret the same text independently. A deterministic comparison finds where they disagree. Then a Skeptic attacks the places where they agree, because shared blind spots are more dangerous than visible disputes. Other agents build examples that tell the competing readings apart, and pick out the few questions actually worth a human’s attention. For a signing policy such a question might be: “Alice approves at 10:00. Her authority is revoked at 10:01. The transfer is about to execute at 10:02. Does her approval still count?” That’s a concrete decision a responsible person can make, and it’s a lot easier to review than pages of formal notation silently assuming one answer. Once decided, it becomes a versioned commitment that downstream code and verification must respect; an unresolved high-risk default becomes an explicit question or an explicit hole, not a majority vote among plausible model completions.[9] The August prototype demonstrates the evidence pipeline on three curated examples; the hive is the next design step, and the thing to measure is whether it actually catches ambiguity while cutting human review effort.[9]

For a fairly simple, isolated function like the bridge minting code, the situation is easier still. It is important enough to the business operating the software that humans—working with AI agents, sure—can sit down and validate a precise formal spec for that exact bit of software and all the pieces around it. Then you have a correct-by-construction implementation of that particular piece.

So that’s all wrapped into the Omega Purple design: red team, blue team, fix the bugs; plus automated code analysis and enough understanding of the domain to identify the pieces of code most critical not to have hacked; rewrite them, if need be, in a more verification-friendly language; iterate with the humans involved to get a detailed spec for the functionality; and then prove that the code is secure against that spec.

“But what if the theorem prover gets hacked?”

One argument I’ve often heard when talking about all this is: What if the theorem prover itself isn’t secure? How can you really, 100%, know? And of course we can’t 100% know anything. I could be dreaming right now. We could all be living in a simulation! And yes, less outlandishly, if the hardware chips are all somehow compromised, then all the software security in the world may not help.

But we can achieve a very, very high level of security this way. The formal verifier—the proof-checking kernel that actually decides whether a proof is valid—is not that much code, and it can be reviewed by a whole bunch of trusted humans in the open-source community. The discipline that goes with it is honest bookkeeping about what is being trusted: the tools each do a distinct job (property tests hunt for counterexamples, model checkers explore bounded behavior, solvers settle precise formulas, proof kernels check proofs), and the hive has to keep those distinctions rather than blur them. An agent’s confidence is not a theorem, and agreement among agents is not a proof checker.[9] The objective is to shrink and expose what has to be trusted and then strengthen it, not to hide a large trusted system behind a small verified one’s reputation.[10]

So net net – I really do think this formal-verification-based approach can essentially solve the cybersecurity apocalypse. We’ll start with products like Omega Purple fixing bugs and replacing the most critical code with formally verifiable code. Then the next step is: for anything that’s really important, replace the whole crappy codebase with a new-style codebase that can be formally verified to do what it’s specified to do. And if you don’t have a formal spec, interact with your agent hive until you get to one. Even if it’s not ultimate perfection, you’re going to have vastly better defense with software that provably fulfills a decent spec—and holes in a spec can be identified by expert humans far more easily than subtle bugs buried deep in an implementation.

Don’t let the AGI’s mind get hacked: ASI:Chain and F1R3FLY

We’ve been thinking a bunch about how to get this next level of security for our core AGI software in particular. If we’re going to launch an AGI, we don’t want the AGI’s mind to be hacked.

Here, however, we have a big advantage over situations involving fixing a lot of old software. The whole design of ASI:Chain, on Greg Meredith’s F1R3FLY infrastructure, was built with formal verification in mind—the smart contracts, the language interpreter, the node code. The smart-contract language, Rholang, starts from a mathematical account of concurrent computation, the rho-calculus, a reflective extension of the pi-calculus; in plain terms, the language is built from the ground up around processes communicating over channels, so concurrency is part of its foundation rather than something bolted on afterward.[5] Rholang’s fresh, unforgeable channel names give it capability-style authority essentially for free: another process can’t manufacture access to a channel just by spelling its name, the access has to be handed over. To be precise about what that buys, it is an authority property, not a promise that data on a public blockchain is confidential; the language’s own tutorial is explicit on the point.[5]

And there’s concrete verification work, not just mathematical ancestry. The Rust node repository documents TLA+ models for its concurrent protocols (TLA+ is a specification language for exploring how a concurrent system can behave), Rocq/Coq proofs of selected algebraic cores (Rocq/Coq is a proof assistant that mechanically checks mathematical arguments), and Kani harnesses for selected Rust logic (Kani is a model checker that works directly on Rust code), alongside property-based and concurrency testing, covering things like authorization and slashing logic, finalized-state monotonicity and fork-choice reasoning. The repository also keeps configurations that reproduce earlier defects, so a model has to show what it rules out rather than merely flatter the implementation.[6] There is still plenty of work to be done – ASI:Chain is in DevNet stage not yet Mainnet, but the trajectory is clear.

The MeTTa, which is both the language-of-thought of our Hyperon AGI framework and the smart contract language for ASI:chain, adds another useful property: MeTTa programs are symbolic structures that other programs can inspect, transform and reason about, which is what you want when the “other program” is an AI doing verification. MeTTa-IL (the MeTTa variant used in ASI:Chain) takes a declared language definition—syntax, types, binding, rewrite rules—and generates executable machinery from it, narrowing the gap where a language’s definition and its implementation drift apart, though generated code is not thereby a verified compiler.[8][9] Put it together and the ASI:Chain direction becomes something more interesting than “agents can pay each other”: contracts accompanied by inspectable evidence of their intended meaning, their formal properties and their implementation identity, with a deployment committing to the hash of that evidence on-chain without publishing every confidential document behind it.[9]

Once we’re running everything on ASI:Chain, we’re a huge step into the future from anything we have now. With the obvious real-world caveats we’ve already reviewed, of course: neither decentralization nor a mathematically elegant language will rescue a compromised signing host sitting underneath them.

Securing the OS itself: AGI on Genode on seL4

Another thing I’ve thought through a bit in this direction is the operating system itself, because Linux kernel bugs are also a major thing now, and a formally constrained agent isn’t well protected if the machine it runs on can overwrite the constraint. There’s a lot of interesting technology here. You can take stuff off Linux and cross-compile it to something called Genode, running on something called seL4. seL4 is a small, capability-based microkernel—the privileged core of an operating system, stripped down to the essential isolation and communication mechanisms—and it has machine-checked proofs of correctness and security for specified configurations, which is a rare thing for any software, let alone a kernel. Genode is an operating-system framework that organizes applications, drivers and services into components with explicit resource allocation and capability-mediated connections between them, and it can run on seL4.[4][10]

So if you have C++ or Rust code without too many weird database or network dependencies, you can use Nix or some similar apparatus to cross-compile it for Genode plus seL4, and then you’re running your AI code on a formally verified operating system. The qualifications have to stay attached: seL4’s proofs don’t automatically verify Genode, or your application, or every machine that can boot the kernel; the hardware and configuration have to match what the proofs actually cover, and the hardware, boot, device-access and side-channel assumptions have to stay visible rather than get hidden behind the microkernel’s reputation.[10]

I’ve worked through what you’d have to do to do this for our MeTTa compilers and runtimes, for the MORK knowledge graph, and for F1R3node, the core blockchain node under ASI:Chain. CeTTa’s core evaluator can be separated from its build-time bootstrap and optional integrations. MeTTaIL’s generators can keep running on the development machine while the language implementations they generate get compiled for Genode. For MORK—the high-performance graph-storage and pattern-matching engine under our MeTTa work—the fast graph and PathMap machinery stays intact while allocation, compact-tree storage and platform-dependent control flow get adapted; the tightly coupled inner operations stay local, since capability isolation doesn’t have to mean an inter-process call for every graph traversal. For F1R3node, the codebase’s encapsulation makes selective substitution realistic: LMDB is a storage backend, not the definition of the ledger, and Tokio’s task machinery is not the same thing as Mio’s operating-system I/O layer, so those isolated parts can be replaced or adapted while preserving transaction guarantees, replay behavior, protocol compatibility and peer authentication.[11]

There’s work there, but it’s all quite plausible—there’s no “rebuild the whole thing from scratch.” I should be clear that these are source-based engineering prospects, not completed ports, and that a successful port only shows a component runs in its target environment; showing it can’t exceed its authority is a separate job, and the two should proceed together. I will link here a brief technical note going through this in a little more detail, for those who are curious.

This fits naturally with OmegaLinux, our medium-term plan for integrating Hyperon, Omega and Nix: Hyperon supplies the cognitive machinery, Omega organizes the agents’ work, Nix provides a disciplined way to assemble the software. Nix—a build system whose central idea is that every artifact is determined precisely by its declared inputs—keeps build-machine generators distinct from target executables, pins toolchains and dependencies, and lets us maintain a Linux reference and a Genode/seL4 target from the same project. It doesn’t prove a compiler correct or authorize a release; it makes the identity and construction of the thing being tested or proved far easier to track.[11][12] The intended deployment discipline then ties together the approved requirement, the formal property, the checked evidence, the source revision, the build inputs, the executable and the capability configuration, so that a changed assumption triggers the relevant revalidation—and an agent may propose an upgrade but cannot approve its own privilege expansion or replace the mechanism that decides whether its actions are allowed.[3][11] That discipline is what turns the layers in Figure 1 from a stack of separately nice technologies into one maintained assurance chain.

The cybersecurity arms race, and what a sane government would do

So there’s a clear path to working our way out of the cybersecurity situation we collectively find ourselves in, and avoiding an actual cybersecurity apocalypse. The issue of course is timing – which is acute because of the arms race dynamic. The hacking agents are getting more and more powerful, and nastier and nastier, and we know what we have to do: step by step, replace it all with formally verifiable code—and AI coding agents are the key to doing that quickly. But we’ve got to do it more quickly than the hacking agents hack everything.

If the government were going to do something intelligent here—not the usual situation—then what it should be doing is not trying to slow down AI. It should be putting massive funding into formal verification via AI, into replacing all the critical software with formally verifiable software, after which all these hacking agents are not such a big problem.

I know Bernie Sanders would rather sentence all of us building superintelligence to twenty years in the hoosegow, but rather than building a fascist surveillance state, it’s going to be a lot more effective to put that money into replacing our software with software that isn’t crap and can be proved to do what it’s supposed to do. And without government funding in this direction—guess what? We’re doing it anyway.

What survival looks like

Like I said, the clarity of this overall path doesn’t liberate us from having to be careful now and do the immediate things to shore up our infrastructure against attack; we’re putting a lot of energy into exactly that at SingularityNET, given what’s happened. But after the short-term shoring-up, you can’t just keep playing whack-a-mole forever, and you can’t protect against every attack the AIs are going to come up with. In the end, the same AI technology that makes attack cheaper is what makes specification, verification and disciplined implementation cheaper too. We just have to choose to spend some of that intelligence on changing the architecture, not only on speeding up the next round of patching.

The goal is not an AI clever enough to guard every crack forever, but a stack whose critical boundaries stay enforceable even when the software on the other side of them is clever, mistaken or hostile.

Sources and publication notes

Supporting links for the draft. Online sources were checked on 27 September 2026; project documents describe the maturity recorded at their respective dates.

[1] AI-assisted attacks. Anthropic, “Disrupting an AI-orchestrated cyber espionage campaign,” 13 November 2025. An attributed incident report, not a claim that all cyberattacks are autonomous. Read the report.

[2] SingularityNET bridge incident. SingularityNET community statement concerning the 19 September 2026 incident; Bitquery Research, “SingularityNET Hack Explained: AGIX, FET and NTX Minted,” 20 September 2026. The $1.5 million estimate, the figures for the other affected chains, and the preliminary AI-agent/AWS assessment in this draft come from the author, not independent confirmation by these sources. Community statement · On-chain investigation.

[3] Omega Purple. Ben Goertzel / BGI Labs, Omega Purple: Agentic Security Office—Product Overview and Design Specification, v1.2, 29 July 2026. Supplied design document; especially the executive summary and sections 4–5, 7.4, 9 and 13. The text describes a design and staged programme, not independently established product outcomes.

[4] Capability-based composition and Genode. Genode Labs, architectural overview: component hierarchy, least authority, explicit connections and application-specific trusted computing bases. Genode overview.

[5] Rholang semantics and authority. F1R3node repository, Rholang README and tutorial, especially the distinction between unforgeable channel names and confidentiality. The tutorial includes historical syntax; only its conceptual authority distinction is used here. Language overview · Channel-name tutorial.

[6] F1R3node verification work and limits. F1R3node Rust README and formal-verification guide. These document selected models, proofs, code harnesses, regression methods and outstanding obligations; the README carries the production-audit warning. Repository documentation was inspected, not its entire proof suite independently rerun. Repository and security notice · Formal-verification guide.

[7] ASI:Chain development context. ASI:Chain documentation, “DevNet Structure & Entities.” Used to distinguish the development platform from a blanket production-security claim. ASI:Chain documentation.

[8] MeTTaIL. F1R3FLY, mettail-rust README. Declarative syntax, types, binding and rewrite rules generate implementation machinery; this is not evidence of an end-to-end verified compiler. MeTTaIL repository.

[9] Plain2MeTTa and the interpretation hive. Ben Goertzel and collaborators, Enabling Spec-Driven MeTTa Development via Multi-Step Plain2MeTTa Translation with Omega Agent-Hive Interpretation, 20 August 2026. Supplied v3 document; especially sections 2, 4–7 and 9. Three curated prototype examples and the proposed generalization are explicitly distinguished. Prototype repository named in the paper.

[10] seL4 proof coverage and assumptions. seL4 Foundation verification overview, verified-configuration matrix and proof assumptions. Guarantees depend on the actual architecture, configuration, theorem and remaining trusted assumptions. Verification overview · Verified configurations · Proof assumptions.

[11] Companion technical note. Toward Provably Secure AGI Infrastructure: Porting CeTTa, MeTTa-IL, F1R3node and MORK to Genode on seL4, using Nix, 27 September 2026, eight pages. Document here.

[12] Nix cross-compilation. Nix documentation, “Cross compilation”: separation of tools running on the build machine from programs compiled for the deployment platform. Nix documentation.