This work proposes CodeSpec, a dual executable specification method for repository-level feature development that builds reliable functional chains from evidence pairing sub-requirement semantics with repository architectures, then compiles them into complementary architecture and behavior specifications that check chain completeness and correctness while preserving design-implementation consistency over long interactions.
Abstract
LLM-based code agents have advanced repository-level software development through iterative interaction with codebases and tools. However, feature development requires integrating new behaviors into existing architectures through coherent cross-component functional chains. Existing agents typically derive such chains through free-form reasoning, often producing unreliable feature designs with incomplete functional chains. Moreover, textual designs are difficult to verify and enforce, making it challenging to maintain design-implementation consistency throughout long-horizon development. We propose CodeSpec, a dual executable specification method for repository-level feature development. It builds reliable functional chains from evidence pairing sub-requirement semantics with repository architectures, then compiles them into complementary architecture and behavior specifications that check chain completeness and correctness while preserving design-implementation consistency over long interactions. On FeatureBench, which targets feature development in existing repositories, CodeSpec achieves 70.7%, 55.0%, and 49.9% pass rates under DeepSeek-V4-Pro, outperforming representative baselines such as Claude Code. Results on the repository generation benchmark NL2Repo-Bench further demonstrate its generalizability.
This work proposes TraceDev, a multi-agent framework for automated software development grounded in use cases that contain multiple functional points and complex semantics, and demonstrates the effectiveness of TraceDev in repository-level code generation from requirements.
Mingyu Chen, Yakun Zhang, Zihao Xie et al.· 0 citations
Repo0 is presented, a continuous structural evolution framework for zero-to-all code generation that maintains an explicit architectural state instantiated as a Dual-Directed-Acyclic-Graph (Dual-DAG), consisting of a requirement-level DAG, a component-level DAG, and their alignment relation.
Silin Chen, Haoyi Teng, Xiaodong Gu et al.· 0 citations
Cross-platform code generation is a critical challenge in modern software engineering, particularly for systems targeting heterogeneous instruction set architectures and operating systems. Although large language models (LLMs) have demonstrated strong capabilities in code generation, existing approaches often suffer from implicit semantic modeling, insufficient handling of platform-specific constraints, and lack of reliable validation mechanisms, leading to unstable and non-compilable outputs in real-world scenarios. To address these limitations, this paper proposes CCGMAS, a multi-agent framework for cross-platform Go code generation. The framework consists of four collaborative agents: a Platform Residue Analysis Agent that extracts platform-dependent semantics and constructs a structured platform residue profile, a Requirement Generation Agent that transforms multi-source code context into a requirement-centered semantic representation with iterative quality optimization, a Code Generation Agent that produces target-platform implementations through multi-candidate synthesis, and a Verification Agent that performs progressive validation and provides structured feedback. By introducing requirement documents as an intermediate semantic layer and incorporating platform residue modeling, CCGMAS enables more explicit semantic alignment across platforms. Furthermore, a feedback-driven refinement loop is designed to iteratively correct errors at different stages, improving both functional correctness and platform compatibility. Experiments on CCGBench demonstrate that CCGMAS reduces the platform residue rate by up to 62.2% in the best case and improves the cross-platform build pass rate by up to 45.0% compared with direct translation baselines.
BRIDGE is presented, a structured prompting framework that decomposes verification into three interconnected domains: Code (implementations), Specifications (formal intent), and Theorem State-ments (constructive correctness claims), and elicits domain-specific intermediate reasoning to connect them.
Robert Joseph George, Carson Eisenach, Udaya Ghai et al.· 0 citations
Vero is introduced, the first benchmark to evaluate joint implementation and proof synthesis at the repository level and an audit mechanism where agents are allowed to formally prove unsatisfiability of provided specification or incorrectness of reference code, which surfaces and corrects latent code and specification errors during curation.
Zhe Ye, Hantao Lou, Yuechun Sun et al.· 0 citations
Creating code specifications is a crucial measure to improve the trustworthiness of many industrial systems implemented in Rust with high security requirements. Because writing specifications requires highly specialized professionals and is time-consuming, the automatic generation of specifications, enabled by large language models (LLMs), has received increasing attention and shown promising results. However, these methods typically focus on partial specification generation (generating proofs after the contract is known) and on extracting dependencies between code modules using predefined relations. This is not suitable for real-world industrial systems where the goal is to generate complete specifications from scratch and where the complex dependencies between code modules are variable. To address this, we propose a multi-agent collaborative framework, StarVerus, to automate the verification of industrial Rust code. Specifically, StarVerus addresses the aforementioned limitations in two ways: 1) In the generation phase, it instructs the LLM to generate all specifications for a given code, and in the repair phase, it uses a cascaded two-stage process of contract alignment and proof repair to correct them; 2) In both the generation and repair phases, it utilizes a function call graph to adaptively obtain bidirectional contextual information (i.e., what it calls and what calls it) for each code module as an additional information source for the LLM. Furthermore, StarVerus introduces a planner-repairer-actor-rewriter multi-agent paradigm to further enhance the proof repair capabilities. Finally, the effectiveness of StarVerus is validated through experiments on benchmark datasets and deployment in a real operating system.
Chao Jiang, Ding Wang, Dugang Liu et al.· Proceedings of the 32nd ACM...· 0 citations