arXiv:2605.12981cs.SEcs.AI2026-05被引 3

用可机器验证的协议管住自动生成的代码,确保可信交付。

Protocol-Driven Development: Governing Generated Software Through Invariants and Continuous Evidence

  • 以协议三元组(结构/行为/操作不变量)定义可接受代码边界。
  • 生成代码需通过协议验证并留下可追溯的合规证据链。
  • 适合需要高可靠性与可审计性的自动化软件开发场景。

自动化程序合成降低了实现成本,但带来了更难治理的问题:如何判断生成的代码是否可接受。自然语言规格模糊,基于样例的测试仅覆盖部分行为空间。单独使用二者均无法提供充分的控制边界。我们提出协议驱动开发(PDD),将核心软件产物从代码变为可机器执行的协议。协议 P = (S, B, O) 定义了结构、行为和操作不变量,其合取限定软件组件的可接受实现空间。在 PDD 中,实现是通过约束搜索发现的可替换实例,只有满足协议并生成可验证合规证据链的实现才被接纳。准入基于协议满足性和记录证据,而非对生成器的信任。对于已部署系统,我们将证据链扩展为动态证据账本,运行时验证器持续追加签名观测、不变量检查与违规记录,使可监控义务得以持续证明。这使实时故障能反馈至生成循环,而不赋予生成器运行时权限。PDD 结合形式化方法、属性测试、运行时验证、策略即代码与软件溯源,构建了自动化软件工程的治理模型。其核心理念是:代码是瞬态的,而协议承载持久权威。

原文摘要 · Abstract (English)

Automated program synthesis lowers the cost of producing implementations but introduces a harder governance problem: determining which generated artifacts are admissible. Natural-language specifications are ambiguous, and example-based tests sample only part of the behavioral space. Used alone, neither provides a sufficient control boundary. We introduce Protocol-Driven Development (PDD), where the primary software artifact is a machine-enforceable protocol rather than code. We define a protocol as the triplet P = (S, B, O), specifying structural, behavioral, and operational invariants. Their conjunction defines the admissible implementation space of a software component. Under PDD, implementations are replaceable realizations discovered through constrained search. An implementation is admitted only if it satisfies the protocol and produces a verifiable Evidence Chain of compliance. Admission is grounded in protocol satisfaction and recorded evidence rather than trust in the generator. For deployed systems, we extend the Evidence Chain into a Dynamic Evidence Ledger. Runtime verifiers append signed observations, invariant checks, and violations to the ledger, allowing monitorable obligations to be continuously attested. This connects live failures back to the generation loop without granting the generator runtime authority. Combining formal methods, property testing, runtime verification, policy-as-code, and software provenance, PDD defines a governance model for automated software engineering. Its organizing principle is that code is transient, while the protocol carries durable authority.

协议驱动生成式编程可信治理

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