Research
Each result below has its own page. A page says in plain words what the result shows and how it was checked. It gives what we found with its limits beside it, says why it matters now, names the published work it builds on, and links the evidence files.
All results
- Random crashes found unclean recoveries in our AI agent's transaction layer; every crash point we chose recovered cleanlyAt random moments, 31 of 2,893 recoveries were not clean, and some undid committed work; at all 29 points we chose in advance, recovery was clean.
- Thousands of candidate code patches scored by proof: each one certified sound, proven unsound, or left undecidedOn models of each check, 2,673 candidate patches of unstated origin are certified sound and 3,077 proven unsound, and two independent solvers agree with every verdict.
- Ultra Ethernet ordered delivery: one recovery design checked in a model against the standard's ruleA model check that one recovery design meets the Ultra Ethernet rule for in-order delivery. Four tools agree, and a naive design is shown to break it.
- Three agent tools can leak a secret together even when every pair of them is safeThree smallest sets of our ten tools leaked a stored secret together, and only one of them is a pair, so a pair-by-pair check over the same three-call sequences would pass the other two.
- The chip netlist whose area and delay are published matches its design: a formal equivalence proofAn open-source tool proves that the gate-level netlist of the lab's admission engine is equivalent to its source design, for every input.
- One protocol rule, compiled into five targets for hardware, kernel, firmware and logsOne state machine compiled to five targets; four, among them chip assertions and C firmware, shown catching their own broken copies where they run.
- Six slightly weakened bounds checks pass random fuzzing, and two coverage-guided fuzzers find all sixSix weakened checks each passed 20,000 random fuzz draws with no hit, and coverage-guided fuzzers found all six in every run.
- Searching for combined Wi‑Fi sign-in attacks without hints: a budgeted search and a complete oneA complete search of all 53,485 combinations of up to three attack families, on ten modelled designs, found no escape; a budgeted search of larger combinations found none either.
- A permission grant cut to a minimum: for one workload every kept permission proved needed, for the other the result is partialThe lab cuts a declared permission grant to a minimal one, then removes each kept permission and re-runs. One workload is certified minimal; one is partial.
Questions, answered plainly
- Who is OrbitalProof for?
- First, AI agent-platform teams whose assistants change real files and databases, and the security teams who decide which tools an assistant may combine. Second, Wi-Fi, Ethernet and chip makers moving to quantum-safe sign-in. To license or acquire a result, write to the address at the bottom of this page.
- What would a buyer get?
- A result with its evidence: the test or proof, the files it was measured from, and its limits stated beside it. We have run the crash test and the tool-combination search only on our own layer and tools; running them on a buyer’s system is untested, and we have not yet done it for anyone.
- Why does OrbitalProof also work on Wi-Fi?
- We lead with AI agents. The network work came from the same practice of testing what breaks and publishing the evidence, here as proofs and automated attack searches for Wi-Fi and Ethernet equipment. It comes second on our home page.
- Can I check the work myself?
- Partly. Each result on this site links to the file its figures come from, and the checker on our home page confirms in your own browser that a file is the one we published. Re-running a result needs our code, which is private.