PaperlayerView exact revision on arXiv

Source-linked AI summary

AssureCode: Structured Justification for Trustworthy Agentic Coding

Logan Murphy, Wilson Sy, Rhys Balevicius, Kelsie Fung, Karenna Kung, Aren A. Babikian, Marsha Chechik

arXiv:2610.29758v1cs.SE

TL;DR

Agentic coding can leave a gap between developer intent and generated software, while evidence such as tests may not establish that the software matches that intent. The paper introduces structured justification rationales and AssureCode to connect intent, formalization, and evidence. Its evaluation finds that one AssureCode execution recovers most concerns surfaced by six merged baseline prompts while also surfacing additional concerns.

  • Problem

    Agentic code generation separates developer intent from produced artifacts, and internally consistent requirements, implementations, and tests may still fail to demonstrate alignment with intent.

    Source: §1 · pp. 1–2

  • Method

    AssureCode uses structured justification rationales, partial formalization, autoformalization, theorem proving, and agentic artifact generation to organize claims, evidence, and validation obligations.

    Source: §3.1 · p. 5, §4.1 · p. 8, §8 · p. 19

  • Results

    A single AssureCode execution recovers most concerns surfaced by six merged baseline prompts while also surfacing additional concerns.

    Source: §5.2.5 · p. 16, §6 · p. 17

  • Takeaways & Limitations

    AssureCode provides a structured mechanism for eliciting and organizing collateral validation obligations during AI-assisted software development.

    Source: §6 · p. 17, §8 · p. 19

    The evaluation used relatively few samples from three benchmarks, mostly small, well-specified programming tasks, and did not assess the practical costs of producing assurance artifacts.

    Source: §5.2.5 · p. 16, §6 · p. 17

Abstract

from arXiv · show

The use of AI-based tools in software development is rapidly changing how software is produced, enabling large volumes of code to be generated with limited human implementation effort. However, this raises fundamental challenges for ensuring that generated artifacts are aligned with developer intent and have been appropriately validated. In this work, we propose the use of structured argumentation in driving AI-assisted software development. Inspired by techniques from assurance engineering for safety-critical systems, we define a language of justification rationales that explicitly relate informal natural language prompts, formal specifications, assumptions about developer intentions, and program analysis evidence in a structured and verifiable format. We then describe AssureCode, a tool-supported methodology for creating such rationales as part of agentic code generation. We provide an empirical analysis of our implementation where we investigate its capacity to contribute towards justified assurance of correctness for AI-generated code.

1 Introduction

Agentic coding separates developer intent from generated artifacts, making trust dependent on explicit justification. The paper introduces structured justification rationales and AssureCode to connect intent, specifications, and evidence during code generation.

1 Introduction

  • Agentic tools can generate code at scale while increasing the separation between developer intent and produced artifacts.Unlike traditional development, developers may be less directly involved in implementation and rely more on requirements, steering, and evaluation.Source: §1 · p. 1
  • Trustworthy code requires clear intent, concrete evidence that properties hold, and grounds for believing the evidence demonstrates alignment with intent.An agent can produce internally consistent requirements, implementation, and tests without demonstrating alignment with what the developer intended.Source: §1 · pp. 1–2
  • Justification rationales explicitly connect claims about program properties to evidence and collateral validation obligations needed to assess evidence adequacy.The approach is inspired by structured assurance cases for safety-critical systems.Source: §1 · p. 2
  • AssureCode combines autoformalization, theorem proving, and agentic artifact generation to construct and use justification rationales during code generation.The paper also evaluates whether the implementation identifies collateral validation obligations for human review before accepting AI-generated code.Source: §1 · p. 2

2 Motivation and Background

Trust in agentic software requires more than passing tests: developers need a clear account of intent, verification evidence, and reasoning that connects the two. Structured assurance cases offer a model, but their manual development must be adapted to agentic workflows.

2.1 Trustworthiness in Agentic Software Development

  • Trustworthiness depends on intention, verification evidence, and justification that the evidence demonstrates alignment with intention.Without clear intention, suitability cannot be distinguished; without verification, behavior cannot be predicted; without justification, evidence may not show alignment.Source: §2.1 · p. 2
  • In agentic development, ad hoc scrutiny of generated artifacts can be inconsistent and cognitively demanding, motivating explicit collateral validation obligations.The deduplication example prompts questions about whether duplicates should all be removed or reduced to one copy, and whether tests cover heterogeneous lists.Source: §2.1 · pp. 2–3

2.2 Structured Assurance Cases

  • Structured assurance cases organize system-safety claims into arguments supported by evidence, with assumptions and context made explicit.The ACC example includes unit-test subgoals for absence of violations and 100% MC/DC, under an assumption about the sufficiency of that coverage.Source: §2.2 · pp. 3–4
  • Because assurance cases are traditionally developed manually over long periods, their formalism and creation process must be adapted to agentic development's rapid iteration and deployment.Source: §2.2 · p. 4

3 Justification Rationales for Agentic Coding

The paper adapts assurance-case argumentation for agentic coding by linking developer intent, formal claims, evidence, and validation obligations. Its rationale model uses partial formalization and permits both proved and human-accepted decompositions.

3.1 Justification with (Partial) Formalization

  • Partial formalization defines only selected symbols, allowing important or straightforward aspects to be formalized while others remain uninterpreted.In the deduplication example, the vocabulary defines nodup but initially leaves preservesOrder and the dedup function uninterpreted.Source: §3.1 · p. 5
  • Each claim pairs a formal proposition with a natural-language statement, supporting both mechanized analysis and developer readability.Claims and their subclaims share a vocabulary; a decomposition is sound when the conjunction of child propositions implies the parent under the vocabulary’s theory.Source: §3.1 · pp. 5–6

3.2 A Formal Model of Justification Rationales

  • A rationale links claims about developer intent to evidence artifacts and pending obligations, distinguishing tool-produced evidence from human-resolved obligations.A human developer also confirms the built-in assertion that evidence and obligations together adequately support a leaf claim.Source: §3.2 · p. 6
  • The model supports two decomposition warrants: a proof of soundness or, when proof is unavailable, human-confirmed obligations and an adequacy assertion.The running example includes a formalization refinement, an input-space partition, and test evidence accompanied by oracle and test-adequacy obligations.Source: §3.1 · p. 6, §3.2 · p. 7
  • Justification rationales differ from natural-language explanations by explicitly connecting claims to implementation artifacts, verification evidence, and the obligations underlying those links.The formalism adapts assurance-case argumentation to justify that a generated artifact satisfies developer intent.Source: §3.2 · pp. 6–8

4 AssureCode: Assurance-Driven Vibe Coding

AssureCode builds a rationale through three incremental stages: intent formalization, argumentation, and evidence generation. Human review and automated reasoning support the process, with Lean used in the current prototype.

4 AssureCode: Assurance-Driven Vibe Coding

  • The methodology is configurable and combines human tasks, LLM agent tasks, and automated reasoning and analysis support.The prototype uses Lean as its formalization backend and theorem prover, while the architecture is designed to accommodate alternatives such as SMT solvers.Source: §4 · p. 8

4.1 Stage 1: Intent Formalization

  • Intent formalization turns a prompt into a partial formal specification, which a human reviews before it initializes the rationale’s first decomposition layer.Formalization is lazy: additional interpretations are introduced only when needed, and some symbols may remain uninterpreted.Source: §4.1 · p. 8

4.2 Stage 2: Argumentation

  • Argumentation develops claims with reusable templates, whose formal subclaims are checked for decomposition soundness in Lean before the rationale proceeds.The prototype offers domain, property, tautological, and freeform decomposition templates; argumentation can stop at a user-set depth or when claims are sufficiently refined.Source: §4.2 · pp. 9–10

4.3 Stage 3: Generation

  • Evidence generation applies analytic templates to leaf claims, organizing generated artifacts, tool analyses, and human validation obligations into an executable workflow.The default testing template can partially prove test-oracle alignment; unresolved alignment remains a human obligation, and template configuration determines task order.Source: §4.3 · p. 10

5 Empirical Evaluation

The evaluation compares AssureCode with an LLM-assisted baseline, “vibe justification,” to examine how each identifies collateral validation obligations. It focuses on obligation coverage and assurance value in the context of the artifacts each approach produces.

5 Empirical Evaluation

  • The baseline asks an LLM to identify concerns a developer should consider before accepting a program based on its passing a test suite.The authors frame it as a practical alternative without a prescribed process for organizing assurance artifacts.Source: §5 · p. 11
  • The evaluation asks how many obligations each approach generates, how well the approaches cover one another’s obligations, and what assurance value unique concerns provide.It also examines whether partial formalization addresses baseline obligations.Source: §5 · p. 11
  • Coverage is assessed in relation to the approaches’ artifacts, and the study evaluates their integration rather than separately testing constituent techniques.The stated aim is not necessarily for AssureCode to outperform the baseline on every measure; comparable assurance would support its credibility as an alternative.Source: §5 · p. 11

5.1 Evaluation Methodology

The evaluation uses sampled Python code-generation tasks and paired runs of AssureCode and vibe justification with the same LLMs. It compares the generated obligations and their associated artifacts using defined coverage and assurance-value assessments.

5.1.1 Evaluated benchmarks.

  • Ten tasks each from HumanEval, LiveCodeBench, and MBPP form a 30-task corpus selected to make manual assessment feasible.Each task includes an English programming problem and a test suite.Source: §5.1.1 · p. 11

5.1.2 Subject LLMs.

  • Four general-purpose LLMs are used, yielding 120 paired evaluations across 12 benchmark–LLM configurations.Both approaches use the same underlying model within each configuration.Source: §5.1.2 · pp. 11–12

5.1.3 Baseline: Eliciting Obligations via “Vibe Justification”.

  • Vibe justification uses conservative and liberal prompts, with three queries per style per trial, producing 720 obligation sets before deduplication.Obligations are deduplicated using embeddings, complete-linkage thresholds of 0.85 for baseline and 0.9 for AssureCode, an LLM judge, and manual review.Source: §5.1.3 · p. 12

5.1.4 Eliciting Obligations via AssureCode.

  • AssureCode runs once per task and LLM with a three-layer rationale and automatic approval of review requests during execution.The extracted obligations include formalization fidelity, decomposition, and test-evidence adequacy concerns alongside associated artifacts.Source: §5.1.4 · pp. 12–13

5.1.5 Comparing the Baseline and AssureCode Artifacts.

  • Coverage judgments are asymmetric: AssureCode artifacts can cover baseline obligations, while baseline obligations alone must cover AssureCode obligations.For unique concerns, the study classifies assurance value as Strong, Fair, or Weak; post hoc review alignment was 96% for RQ2, 100% for RQ3, and 84% for RQ4, with RQ4 judgments consistently conservative.Source: §5.1.5 · p. 13

5.2 Results

AssureCode provides comparable assurance support to vibe justification, with asymmetric obligation coverage and more unique concerns; formalization contributes substantially to that coverage. These findings are bounded by proxy measures and evaluation on small, self-contained tasks.

5.2 Results

  • Across 12 configurations, neither approach consistently produces more obligations, although AssureCode produces more in 8 and fewer in 3.Average counts per configuration range from 4.4 to 10.5 for AssureCode and 5.0 to 9.4 for the baseline.Source: §5.2.1 · p. 13, Table 1 · p. 14
  • AssureCode covers at least 90% of baseline obligations when partial coverage is included, while baseline coverage of AssureCode obligations is lower.AssureCode's full coverage ranges from roughly 72% to 88%; baseline full coverage of AssureCode obligations ranges from roughly 33% to 80%.Source: §5.2.2 · p. 14, Figure 5 · p. 15
  • Formalization contributes to a majority of covered baseline obligations in 8 of 12 configurations, alone or alongside AssureCode obligations.Direct obligation-based coverage also remains common; excluding formalization-only resolution narrows the difference between approaches.Source: Figure 6 · p. 15
  • AssureCode raises 343 unique concerns versus 131 for the baseline, with 83% rated at least Fair and more Strong concerns in absolute terms.Baseline-only concerns were more often rated Strong (43% vs. 24%), while AssureCode-only concerns were more often rated Fair (59% vs. 41%).Source: §5.2.4 · pp. 14–15, Figure 7 · p. 16

5.2.5 Summary of Observations .

  • The approaches largely converge on concerns, but coverage is asymmetric and unique concerns vary in quantity and quality across models and benchmarks.The authors conclude AssureCode offers comparable assurance support through a more structured process, not uniformly more valuable obligations.Source: §5.2.5 · p. 16
  • Obligation counts proxy scope, usefulness ratings do not establish real defects, and the small, self-contained benchmarks may not generalize to larger projects.Coverage percentages also depend partly on obligation granularity; results may shift because each task was run only once.Source: §5.2.5 · pp. 16–17

6 Discussion

AssureCode achieved comparable assurance support to prompt-based vibe justification, recovering most concerns found through multiple unstructured prompts while surfacing additional ones. The evaluation leaves generalizability and practical costs open.

6 Discussion

  • A single AssureCode execution recovered most concerns identified through multiple unstructured prompts while also surfacing additional concerns.The evaluation found comparable assurance support to a practical vibe-justification baseline.Source: §6 · p. 17
  • Coverage analysis attributes this support to complementary roles for formalization artifacts and validation obligations.Source: §6 · p. 17
  • The evaluation used relatively few samples from three benchmarks focused primarily on small, well-specified programming tasks, limiting evidence about generalization to realistic projects.Source: §6 · p. 17
  • Only four high-capability LLMs were evaluated, and practical costs such as token use, developer effort, and effects on review remain unmeasured.Source: §6 · p. 17

7 Related Work

AssureCode relates generation, formal methods, and human validation through structured justification rationales. Its approach adapts assurance-case techniques to agentic software development and differs from prior work in how intent and evidence adequacy are handled.

Trustworthy Agentic Software Development

  • AssureCode integrates analysis, proofs, and human–AI collaboration, relating these activities through collateral validation obligations and structured justification rationales.Unlike an earlier proposal by some of the authors, it uses rationale development to drive code generation rather than arguing for adequacy post hoc.Source: §7 · p. 17
  • Unlike TiCoder, AssureCode formalizes intent as a machine-checkable specification and makes evidence adequacy and residual assumptions explicit collateral validation obligations.The prototype currently supports functional testing, though the approach is not limited in principle to testing as evidence.Source: §7 · p. 18

Formal Methods for Agentic Coding

  • Unlike FORGE, which derives formal artifacts from generated code, AssureCode formalizes intent from natural language and treats formalization fidelity as a validation obligation.Source: §7 · p. 18

Agentic Assurance Case Development

  • AssureCode adapts assurance-case techniques to agentic software development, complementing work that uses LLMs to improve safety-assurance practice.Source: §7 · p. 18

8 Conclusion

The paper introduces justification rationales and AssureCode, which creates them during agentic code generation using autoformalization, theorem proving, and agentic artifact generation. Its evaluation suggests comparable assurance support to prompt-based vibe justification, while identifying important open questions about scope and practicality.

8 Conclusion

  • Justification rationales make explicit claims about generated code, supporting evidence, and collateral validation obligations developers should address before trusting the code.Source: §8 · pp. 18–19
  • AssureCode creates these rationales during agentic code generation through autoformalization, theorem proving, and agentic artifact generation.Source: §8 · p. 19
  • The evaluation suggests comparable assurance support to prompt-based vibe justification through partial formalization and structured generation and organization of validation obligations.Source: §8 · p. 19
  • Future work includes user studies, extending rationales beyond functional correctness, and applying AssureCode to larger projects with component interactions.Source: §8 · p. 19

Related papers

Loading 2610.29758v1…