One interesting aspect of how AI produces code (or produces hardware) is that it does not need the abstraction barriers required by humans or organizations. A famous (or infamous) example is the ISA which split the world into software (Microsoft) and hardware (Intel). Now we are in a position to radically rethink the hardware/software boundary, and to some extent erase the difference between hardware and software. When an AI is given a specification of some computation it can now use carefully curated components with formal semantics and proved correct algebraic laws about their composition to produce entirely new systems that are a blend of hardware and software, all produced from one coherent description, with the final result translated into C/Rust or Verilog which is correct by construction, a dream of 80s software research which has now become a practical reality. So AI and verification is going to break down the silos and barriers that have driven up the cost of system design, instead putting hardware/software on a spectrum from which we can pick the point that matches our power, area and performance requirements.

Now we can totally rethink how to do verification. Instead of having a specification and some artifact created somehow and trying to relate the specification to the implementation, we can start with the specification and iteratively refine it, applying proved correct transformations, adding additional detail (pipeline stages, registers, caches etc.) until we have the concrete implementation we desire. There is nothing to prove about this implementation, because it is correct by construction, finally realizing the 80s dream of the Bird-Meertens formalism. Back then we did not have the proof automation to make refinement from specification to implementation practical. Today we do.