Harmonic 宣称两年内代码全面形式化验证，管理 300 万行代码者逐条反驳

jiriknesl 反驳 Harmonic 两年内让所有代码完成形式化验证的宣称，指出验证只能证明代码符合规约，无法排除规约本身错误。证明 1 行代码需 5-50 行证明，管理超 300 万行代码者不可能研读 6000 万行证明，更合理的做法是仅验证关乎安全和关键业务的几千行代码。