Formal-Methods

今天关注 AI-native 软件工程里的两条更硬核路径：用 specification-first + verification loop 推进超大规模重构，以及让 coding agent 同时生成实现与机器可检查证明。