Incompleteness and Autonomous Satellites: A Pilgrimage to Gödel
Two talks in London, three doorways in Vienna, and why a logician's limits are the design spec for machines you can trust.
In June I flew to London to talk about machines that have to think for themselves. When the talks were done, I flew to Vienna and went looking for three of Gödel’s homes, where he lived a hundred years ago. This is the story of why those are the same trip.
I run Godel Space. We build the intelligence that lets a satellite decide, on its own, what is worth looking at and what is worth sending home. That sounds narrow. It is not. It is a small, brutal version of the question every autonomous system will eventually face: how do you trust a machine that is making decisions somewhere you cannot reach?
I gave two talks in London that week, and both circled that question.
The bottleneck is not the sensor
The first talk was on the first day of EDGE AI London. The room was full of engineers who put intelligence onto hardware that runs far from any data center, in places where the network is slow, contested, or gone. I made one argument: the bottleneck in space is not the sensor. It is the architecture.
The problem fits in two sentences. A single satellite imaging at capacity produces gigabytes in one pass, and the links that move data between satellites carry roughly a hundred bits per second. The math does not work.
So the industry tells itself a comforting story. We will bring the data down and process it on the ground, and it will be fine. It is fine for archival science. It is not fine when a wildfire is moving or a flood is spreading and the time between collection and a usable answer runs to hours. By the time the image reaches an analyst, the world inside the image has changed.
The fix is not a bigger pipe. It is to stop shipping pixels and put the brain on the satellite. We run NASA’s geospatial foundation model, Prithvi, on a board that costs two hundred and forty-nine dollars and draws about twenty-five watts. On that board sit three cooperating agents. One perceives: it turns raw multispectral imagery into a compact representation. One triages: on a tight, fully logged set of rules, it decides whether a scene is fire, flood, change, or nothing worth the power. One communicates: it sends a small structured alert to the ground, a detection and a confidence score measured in kilobytes, not the gigabytes of the raw scene. Send the insight, not the image.
The three agents are the part people notice. The part that matters is the system around them. A foundation model is a feature extractor, and the model itself is close to interchangeable now. What is not interchangeable is the orchestration: deciding what to process and what to skip, which detection earns a downlink slot and which waits, when to act and when to defer to the ground. We build the satellite to take actions, not only to run inference, with an auditable seam between what the system sees and what it decides. That orchestration layer is the product, and the moat. The machines get smarter every month. The systems around them do not, and closing that gap is the work.
The design rule underneath all of it is unglamorous. Robust first, capable second. In orbit there is no retry and no human leaning over to fix it. A system that fails in a known, bounded way beats one that occasionally dazzles and then fails in a way nobody planned for. We validate that on real hardware, against more than eight hundred labeled scenes, before we call anything done. Runs in a container and runs on the board are different sentences.
[IMAGE 1 — the benchmark slide “Three Engineering Problems, on Real Hardware” from the talk. Caption: Jetson Orin Nano Super 8 GB, Prithvi-EO-2.0, TensorRT FP16. 68 ms per tile at 25 W, about 100x faster than the PyTorch baseline, 0.9947 cosine fidelity to full precision, no thermal throttle at 62 C peak. Validated on HLS imagery from NASA and USGS.]
[IMAGE 2 — ThomaMedia-2606080543.jpg: on stage at EDGE AI London with the “Three Agents on Orbit” slide.]
I built this for the hardest version of the edge, the satellite, where the power moves with the orbit, the link disappears for long stretches, and nothing can be patched mid-flight. The lesson travels down to every machine that has to act where help is not coming.
Are we ready for autonomous edge systems?
The next day I sat on a panel at Hardware Pioneers Max, moderated by Pete Bernard of the EDGE AI Foundation, with David Aronchick of Expanso and Professor Tinoosh Mohsenin of Johns Hopkins. Pete put the question plainly: are we ready for autonomous edge systems?
[IMAGE 3 — 0f9929a6-dc98-467e-b7af-1e45e344e77e.jpg: the Hardware Pioneers Max panel, with Pete Bernard, David Aronchick, Tinoosh Mohsenin, and me.]
David has spent years on the problem of moving computation to where the data already is, instead of dragging the data to the computation. He drew the highway. Tinoosh works at the other end of the stack, on making the silicon itself sip power while it runs real models. She made the engine efficient. My job on that stage was to talk about the brakes, and about who is allowed to hold the wheel.
Because the honest answer to “are we ready” is that the gap is not compute. We have the chips and the models. The gap is that most edge AI is autonomous in name only. It runs inference locally and still phones home for every decision that matters. Real autonomy means the system assesses its own confidence, calibrates, and decides alone, and degrades in a predictable way when the power drops or the buffer fills. That is a harder kind of readiness.
I gave the room the line I had been sharpening for weeks. Autonomy is not the absence of control. It is intelligence acting inside the limits you set.
In practice that means four things, borrowed straight from security engineering. Give the system the least authority that still lets it work. Make its actions reversible. Write hard conditions that stop it. Log everything it does so a human can answer for it later. An agent is not a mind to be reasoned with. It is an amplifier, and the work is to govern the amplification. The future of this field will not belong to the smartest model. It will belong to whoever builds systems that can sense, reason, decide, and act responsibly in the real world, and prove it afterward.
That is the argument I carry into every room. It is not original to me. It is a hundred years old.
Vienna
I had a free week between London and home, and three old friends willing to meet somewhere in Europe. I picked the city where Kurt Gödel grew up. Suman flew in with me. Hansraj came by train from Prague. We kept an apartment out in Simmering and rode Tram 71 into the old town like everyone else. The reunion would have been reason enough to go. That week I also stood in the rooms where Beethoven and Mozart once worked, a few minutes away, though that is a different essay about a different kind of structure.
But I did not choose Vienna at random. I named my company after Gödel, and I had never stood where he worked. So on the one full day we had, I walked to the three homes where he lived as a student. Florianigasse 42. Frankgasse 10. Lange Gasse 72. Each one wears a small dark plaque.
[IMAGE 4 — IMG_2079.HEIC: pointing up at a Gödel plaque on one of the three homes.]
[IMAGE 5 — IMG_2085.HEIC: Florianigasse 42, the house number beside the dark Gödel plaque.]
Some of that walking ended in a coffeehouse. Vienna did much of its hardest thinking over coffee, and the Vienna Circle, the philosophers and mathematicians whose meetings the young Gödel attended, argued out their ideas in cafés as much as in any seminar room. The one where Gödel first spoke his incompleteness result aloud to that circle, in 1930, was the Café Reichsrat, and it is gone now. Café Central, where those same minds also gathered, is still serving. I stopped in for a coffee, in the kind of room where a quiet man could unsettle all of mathematics between two cups.
[IMAGE 6 — IMG_2026.HEIC: Café Central.]
On Lange Gasse 72, someone has carved one of his consistency theorems into the stone beside the door, a line of formal logic on the wall of an ordinary building:
ZF ⊢ Cons(ZF) ↔ Cons(ZF + CH)
If set theory is consistent, it stays consistent when you add the Continuum Hypothesis. A claim about what a formal system can and cannot settle about itself, mounted at eye level next to a doorbell.
[IMAGE 7 — the Lange Gasse 72 plaque with the carved formula.]
In 1931, a few streets from those addresses, Gödel proved the thing that still unsettles anyone who builds systems for a living. Any formal system powerful enough to be useful contains true statements it cannot prove from within. Worse, and this is the part that matters for anyone building autonomous machines, such a system cannot prove its own consistency from inside itself. In the notation he left on these walls: for a consistent system T rich enough to do arithmetic, T ⊬ Con(T). You do not get both complete and self-certifying. You never did.
Incompleteness is the design spec
For most people that is a curiosity from a math class. Standing in front of his door, it stopped being a curiosity and became a design spec.
I had spent the week arguing that you cannot make an autonomous system both fully capable and provably safe, so you stop pretending you have closed it and you govern it instead. Gödel proved, ninety-five years ago, that no system rich enough to matter can fully account for itself from the inside. Those are the same statement. One is about arithmetic and one is about a satellite, but the shape is identical.
So you stop chasing the closed, complete, self-certifying machine. It is not coming. You do the other thing. You bound what the system can do, you log every move it makes, and you keep final authority on the ground with a person who can answer for it. The incompleteness is not the obstacle to autonomy you can trust. It is the blueprint for it. That is why the company carries his name, and standing on Lange Gasse I finally felt the reason instead of just knowing it.
Where this goes
The next decade in orbit will not be won by whoever flies the most satellites. It will be won by whoever flies the most autonomous ones, and autonomy you can trust where the link goes dark is as much a problem of governance as of compute. The hardware is here. The architecture is the work, and the governance is the moat.
That is what I am building at Godel Space. If you operate satellites, build the buses they ride on, fund the hard missions, or answer for outcomes in places where no help is coming, I would like to talk.
I named the company for a man who proved the limits of formal systems. I have come to think those limits are exactly where the trustworthy machines get built.
Watch the panel (Agentic AI Meets the Physical World, Hardware Pioneers Max): youtube.com/watch?v=PcmHN-prBNQ