I was hoping that the basebands and firmwares would get formally verified. Maybe they will ... with AI-written proofs!