If I could burn through an enormous number of tokens

Beginners
1

I would give the latest and most capable available language model a very large token budget and use it to try to create a complete open-source operating system based on the seL4 microkernel.

First, the model would analyze the code and documentation of:

  • seL4,
  • seL4_libs,
  • sel4-tutorials,
  • sel4test,
  • Genode and the related genode-* repositories.

It would then analyze the Linux source code. The goal would not be to port the whole of Linux or support every existing device. Instead, it would gradually adapt selected drivers for the most commonly used current hardware, along with useful file systems and other subsystems, so that they could work in an seL4-based environment. The resulting system would be released as open source, in compliance with the licenses of all reused code.

The model would work iteratively: analyzing code, proposing an architecture, porting small components, compiling them, running tests, examining errors, and making corrections. Each working component would become the foundation for the next stage.

This would be a large and long-running project, requiring an enormous number of tokens, access to many repositories, and the ability to compile and test code autonomously. It would also require access to real hardware for testing and debugging at least some of the drivers. At the same time, it would be an interesting test of whether an LLM-based agent could manage a large systems-programming project while maintaining a coherent architecture throughout its development.

Would the latest and most capable model already be able to complete a significant part of such a project if token and compute costs were not constraints? What would be the greatest obstacle: the size of the codebase, maintaining a long-term plan, testing and debugging drivers on real hardware, formal verification, or the limitations of today’s AI agents?

2

Even with unlimited tokens/compute, the bottleneck isn’t the codebase size, current agents can already ingest and reason over huge repos fine. The real wall is long-horizon coherence: as the project grows across sessions, agents drift from the original architecture, accumulate small inconsistent decisions, and start “fixing” things by contradicting earlier design choices they’ve technically still got in context but stop weighing correctly (this shows up a lot in recent long-horizon agent benchmarks, often called context rot or state drift). Unlimited tokens actually makes this worse before it makes it better, since a bigger context window doesn’t stop the model from losing track of which earlier constraint matters right now.

The hardware/driver testing piece is the other hard wall, and it’s not a token problem, it’s that debugging real driver behavior on physical hardware needs a feedback loop (scope traces, intermittent timing bugs, hardware quirks undocumented anywhere) that no amount of code analysis substitutes for. Formal verification of an seL4-based system is a separate research-grade skill in itself (that’s literally what makes seL4 seL4), and current agents are nowhere near reliably producing verified proofs for novel code, not a compute problem, a capability gap. So ranking your list: long-term architectural coherence and driver/hardware debugging are the real obstacles, codebase size and formal verification are secondary (verification specifically being closer to “not solved” than “hard”).