I'm curious about challenges (what's bad with AM broadcast in an unmanned tunnel?) and why the formally verified killswitch was necessary?