Google's robot hits 96% on car brackets, and AI writes 6 million lines of Lean
Google DeepMind's Mercedes-Benz robot pilot reached 96% success, which also means 4% non-success. AlphaProof Code produced six million lines of Lean for Signal, with humans checking the specifications.
Google DeepMind reported two engineering results on November 10. A Mercedes-Benz pilot with Apptronik handled automotive brackets with 96% success. AlphaProof Code generated more than six million lines of Lean for Signal's cryptographic protocol.
The robotics announcement and AlphaProof Code announcement show Google applying AI inside defined industrial and verification workflows.
CTOL's view is that the integrated workflow is the useful unit of assessment, more than the underlying model alone. The robotics project combines models, a specific robot and a physical task. The formal-verification project combines AI-generated proof material with expert-reviewed specifications. Both are bounded applications of AI, and neither shows unrestricted autonomy.
Factory operators should run controlled trials of the robotics result, measuring exception recovery and completed throughput. Security engineering teams should evaluate which formal claims AlphaProof Code's artifacts establish and how much specialist checking is required.
Robotics: the operational test behind 96%
Google says Gemini Robotics 2.5 was evaluated across more than 200 tasks. The 96% success rate belongs to one Mercedes-Benz proof of concept. There, Apptronik's Apollo 2 picked and packed automotive brackets using Gemini Robotics ER and the Robotics 2.5 actions model.
Google calls the Mercedes work a pilot or proof of concept and says the model is rolling out to robotics partners. The more than 200 evaluated tasks are not presented as the denominator of the bracket result.
On Google's reported success measure, 96% also means 4% non-success. An industrial buyer's next question is concrete: how often must the robot be reset or assisted, and what does that do to accepted output per hour? The result supports testing this specific workflow, but the reported success rate cannot yet be converted into a production cost.
AlphaProof Code: generation is only part of verification
AlphaProof Code addresses a different engineering problem. Google describes a formal-verification framework that involves multiple language models, human experts and AI agents.
According to Google, agents powered by Gemini Carbon generated more than six million lines of Lean for Signal's cryptographic protocol over a reported four-week project. Humans reviewed the specifications, and about 1% of the codebase was flagged for a second look.
That 1% is neither a defect rate nor a measure of the full review burden. The positive result is substantial generation of formal proof material within a process that involved human experts and specification review.
For a verification team, the decision turns on three questions: which protocol properties were specified, what the resulting artifacts establish and what checking remains necessary. Success is measured by assurance against defined claims, and the volume of generated lines says little about that.
What changes the assessment
As of November 10, 2026, CTOL's view is that Google has demonstrated useful progress in task-specific AI integration, with moderate confidence. That judgment rests on the named robotics pilot and the documented human involvement in the formal-verification project. It makes no assumption that either system is ready for unconstrained deployment.
The assessment would strengthen with a dated partner report showing sustained bracket-handling throughput and exception recovery. A dated technical account mapping AlphaProof Code's formal claims to completed verification and human review requirements would do the same. Those observations would show whether the reported engineering results translate into repeatable operating or assurance value.