“After the agents generated 6.5 million lines of Lean code, they undertook an auditing pass and flagged bits that required human review.”
This is a rare AI launch with an actual result attached. The proof assumes perfect cryptography, so it says the design is right, not that your messages are safe. And 6.5 million lines of machine-written proof is only as good as the human-written spec it checks against. The hard part was always deciding what to prove. That part still needs people.