专题：imandra

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