专题：code-verification

文章提出了技术、认知、意图三层债务模型，阐释了将 LLM 纳入 Kahneman 双系统思维形成的三系统认知框架，并指出 AI 代理会把重点从编码转向验证。通过实验验证模型预测力，讨论了代码未来的语言趋势以及验证驱动开发的重要性，呼吁人机协作重塑团队工作流。

Imandra CodeLogician 是一套把 LLM 与 Imandra 形式化引擎结合的原型系统，能够把自然语言需求自动转化为可验证的 DSL 代码并生成归纳证明。它提供可插拔的模型后端、即时错误回馈以及一键 Docker 部署，适用于安全审计、教学和快速原型迭代。项目已开源，配套示例展示了从需求到定理证明的完整流水线。