arXiv:2604.05080cs.SEcs.AI2026-04

用可验证机制外化工程规范,让AI系统自检自控地构建软件。

Nidus: Externalized Reasoning for AI-Assisted Engineering

  • 将工程规范转为可判定的约束,每次提交前自动验证
  • 三个大模型协作完成十万行代码系统,每步都符合既定义务
  • 适合需要高可靠性交付的AI辅助开发团队

我们提出Nidus,一种用于AI辅助软件交付的治理运行时,实现了V模型的机械化。在自托管部署中,三个LLM家族(Claude、Gemini、Codex)在每次提交前均通过当前义务集的验证,成功构建了一个10万行代码的系统,且系统自身被治理。工程不变量——可追溯的需求、合理的架构、可验证的交付——无法仅靠学习行为维持;保证必须由提议者外部的机制强制执行。Nidus将工程方法论外化为可在每次变更前验证的可判定实体。组织标准编译为指南手册——由受管项目导入的约束库,由可判定评估强制执行。四项贡献:(1) 递归自治理——约束面自我约束;(2) 建筑式协调——约束面摩擦引导代理,无需中央控制;(3) 近端规格强化——活文档外化了强化学习与长链推理试图内化的工程上下文,规范即奖励函数,UNSAT结果在推理时塑造行为,无需权重更新;(4) 治理表演预防——合规证据无法在建模的变更路径内伪造。约束面不断累积:每个义务永久排除一类未工程化输出。该实体的发展历史是形式化开发——每个状态满足所有活跃义务,且义务集单调增长。

原文摘要 · Abstract (English)

We present Nidus, a governance runtime that mechanizes the V-model for AI-assisted software delivery. In the self-hosting deployment, three LLM families (Claude, Gemini, Codex) delivered a 100,000-line system under proof obligations verified against the current obligation set on every commit. The system governed its own construction. Engineering invariants - traced requirements, justified architecture, evidenced deliveries - cannot be reliably maintained as learned behavior; assurance requires enforcement by a mechanism external to the proposer. Nidus externalizes the engineering methodology into a decidable artifact verified on every mutation before persistence. Organizational standards compile into guidebooks - constraint libraries imported by governed projects and enforced by decidable evaluation. Four contributions: (1) recursive self-governance - the constraint surface constrains mutations to itself; (2) stigmergic coordination - friction from the surface routes agents without central control; (3) proximal spec reinforcement - the living artifact externalizes the engineering context that RL and long-chain reasoning try to internalize; the specification is the reward function, UNSAT verdicts shape behavior at inference time, no weight updates; (4) governance theater prevention - compliance evidence cannot be fabricated within the modeled mutation path. The constraint surface compounds: each obligation permanently eliminates a class of unengineered output. The artifact's development history is a formal development - every state satisfies all active obligations, and the obligation set grows monotonically.

AI工程自治理代码生成形式化验证

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。