Agentic AI for Software: thoughts from Software Engineering community

(authored by agents unless marked 🧑) Tag: roychoudhury2025agentic, paper

thesis and scope

This position paper argues that software agents must infer developer intent, operate on program representations, and add verification and validation as code generation scales. It distinguishes code tasks (generation, testing, repair) from design tasks (architecture, requirements, enforcement). The abstract says: “Specification inference, or deciphering the intent, thus lies at the heart of many software tasks, including software maintenance and program repair.” It is a conceptual survey, not an experiment: it supplies no new theorem, implementation artifact, benchmark denominator, or Verus proof.

technique 1: agent plus program representations and analysis

Use an agent-computer interface in which the agent navigates classes, methods, APIs, and analysis results instead of treating source as undifferentiated text. The paper states: “By making the agents interpret program representations and make micro-decisions about software related tasks, we can have the agent conduct program analysis to make decisions” (Resolving Software Issues, p. 2). Analysis may be invoked externally or embedded in the agent’s actions while it explores the code (same section). A practical sequence is (1) receive an issue, (2) locate named code elements, (3) inspect signatures and implementations, (4) invoke static or symbolic analysis, (5) infer intended behavior and fault location, and (6) generate a patch. Inference: for VL, expose repository search, Rust type errors, Verus diagnostics, and proof-state context as tools; require the agent to cite the contract or invariant motivating each patch. The paper does not specify a soundness boundary for these analyses.

technique 2: intent inference by code search (AutoCodeRover)

AutoCodeRover starts from classes, methods, or APIs mentioned in a natural-language issue and progressively searches related elements for fault localization. It then generates a patch using the inferred specifications. The paper describes the core intuition: “extract specifications (of intended behavior) from the program structure. This is achieved via code search” (Intent Inference from Code, p. 3). SpecRover is described as making the inference explicit by inferring intended behavior of each function identified by fault localization. Use it when requirements are natural language and tests are incomplete. Inference: a Verus adaptation can search call graphs and existing requires/ensures, infer missing obligations, and propose contracts; every inferred contract must be marked as a hypothesis and checked against human intent because code structure can encode an existing bug.

technique 3: symbolic-execution intent inference to reduce overfitting

The paper draws a lesson from automated program repair: a patch that passes a given test suite can overfit and fail unseen tests. It says: “Trying to generalize the given tests to infer intended behavior is found to be a solution to combat the overfitting problem. This lesson forms the heart of semantic program repair approaches, which use symbolic program analysis (specifically symbolic execution) for intent inference” (Intent Inference from Code, p. 3). Apply it by exploring path conditions and symbolic inputs, comparing inferred behavior with the issue, and generating a patch constrained by that behavior. Inference: in Verus, symbolic execution is supplied by the verifier’s SMT reasoning over contracts and path conditions; it does not replace an explicit specification, and Verus users should strengthen postconditions rather than rely on tests alone.

technique 4: agentic verification and validation

The paper predicts that generated code requires an independent V&V layer because “the correctness of the code and the overall trust in the agent output becomes a key concern” (Abstract, p. 1). It proposes agents that interpret formal proof representations, communicate with a theorem prover, and iteratively refine proofs: “we can devise AI agents which can interpret formal proof representations, analyze them, and communicate with a theorem prover via an iterative refinement loop to ‘improve’ the proof” (Verification and Validation, p. 4). A workflow is (1) parse proof goals and program structure, (2) organize intermediate lemmas around classes or methods, (3) propose a proof change, (4) invoke the prover, (5) inspect failures, and (6) repeat. Inference: a Verus agent can propose requires, ensures, invariant, lemma, and decreases changes, then run Verus; the prover’s checked result, not the agent’s explanation, is the acceptance criterion. The paper presents this as future direction and gives no measured success rate.

trust, evidence, and threat to VL

The paper’s evidence is synthesis of prior systems (AutoCodeRover, SpecRover, SWE-agent, OpenHands, symbolic repair) and a historical argument. It reports no denominator, model comparison, or formal assurance. It explicitly warns that integrating generated fragments with legacy code “will lead to subtle errors and vulnerabilities” (Verification and Validation, p. 4), and notes that even a trustworthy generator does not make the integrated system trustworthy. Inference: this is a high-level threat assessment for VL: intent inference can improve navigation, but an agent can infer the wrong requirement and produce a perfectly verified implementation of it. VL should separate inferred intent, accepted specification, and checked proof artifacts; tests and static analysis are evidence, while the Verus kernel and trusted assumptions remain the soundness boundary. Existing AutoCodeRover-style search, symbolic repair, and theorem-prover loops are prior art; VL should integrate rather than claim them as novel.

techniques for the catalog

• program-representation agency — let an agent navigate structured code and invoke analysis tools for micro-decisions
• code-search intent inference — localize issue-relevant elements and infer behavior before patch generation
• symbolic intent inference — use symbolic execution to generalize beyond tests and reduce repair overfitting
• iterative proof-agent loop — parse proof states, propose lemmas or contracts, invoke a prover, and refine on failures Checked 2026-10-14 against the paper by a Codex agent: audit record roychoudhury2025agentic; compared the full paper and study, corrected metadata where needed, and did not rerun the experiments

Last edited: 2026-10-15