Now that LLMs are capable of generating code like we expect humans to, how will the role of the software engineer evolve? No one knows for sure, but Jevon's paradox, which has proven itself time and time again, states that as the unit cost of something (in this case, writing code) goes down, the total demand increases. Thus, if we end up with an unprecedented amount of code, how do we ensure our systems don't collapse under their own weight?

Not only code has gotten easier to generate, so has mathematical proofs. Tools such as Lean, SAT/SMT solvers, differential testing, and Rust have recently gained popularity as key pillars for making sense out of the complexity of the AI era. Mathematical proof of correctness lets the team move fast without breaking things.

Using LLMs to generate Lean proofs is very similar to Kubernetes letting you focus entirely on the desired state instead of how to get there. In the second decade of Kubernetes, how can the cloud native community answer the challenge of ever-increasing complexity, with possibly tons of newly-contributed code being AI-generated? Can formal verification stand up to the challenge and the community rally around it?