We have proof automation now

# Summary Dependently-typed languages like Coq (now Rocq) and Lean can formally encode and enforce subtle invariants through their type systems, but have remained niche because proving these invariants requires enormous time investment—the seL4 project spent 10 times longer on proofs than on actual implementation. Recent advances in proof automation, particularly through AI and machine learning approaches, now promise to dramatically reduce the manual effort required, potentially making these powerful type systems practical for wider use.