Tackling technical debt at scale with autonomous mode in Kiro Web

Every software development team has experienced the tension between maintenance and building new features: time spent on one is time not spent on the other. For open-source maintainers, this challenge is even more acute with smaller teams, larger user bases, and a backlog that never stops growing. In formal verification, the use of mathematical techniques to prove properties of software and the complexity of the domain makes this especially painful. The AWS Automated Reasoning Group maintains or is a principal contributor to several open-source formal verification tools, including the Kani Rust Verifier and the C Bounded Model Checker (CBMC). In November 2025, when we began the work described in this post, these repositories had 916 open issues, with maintenance tasks accumulating faster than the team could address them while continuing to advance core verification capabilities.

Traditional approaches to technical debt force a choice between allocating developer time to maintenance (and slow feature delivery) or letting debt compound. Interactive AI coding assistants help speed up individual tasks but still require a developer actively in the loop for every step. We wanted a third option that takes a maintenance task end-to-end, from reading the issue to opening a pull request, so engineers only step in at code review, where their judgment matters most. That tool is Kiro’s autonomy mode in Web, an agentic software engineering tool that can perform a range of tasks, including maintenance, while engineers focus on higher-value work. Here is what that looks like in practice. Over two months, Kiro submitted pull requests addressing 87 open issues across our repositories, a volume approaching what the team had addressed during the prior 22 months (about 2 years).

In this post, we describe how we set this up, share two case studies in detail, and explain how to use Kiro autonomously on your own repository.

Kiro in autonomous mode operates autonomously in its own secure cloud development environment while integrating with existing workflows. Assigning work to Kiro is simple: describe the task on app.kiro.dev, add the kiro label to a GitHub issue, or mention /kiro in a comment. Kiro then clones the repository into an isolated sandbox, analyzes the issue and related code, breaks the work into steps, implements the changes, runs the full test suite, and opens a pull request. Every pull request is subject to the same approval requirements as human-authored code, including passing CI and code-owner review. Kiro does not have merge permissions and cannot bypass branch protection rules.

The tasks most suitable for this approach are those with clear acceptance criteria and isolated scope. Dependency updates, well-reproduced bug fixes, and documentation improvements are all good starting options. Tasks requiring architectural decisions or crosscutting refactors are better left to humans. When Kiro encounters ambiguity, it asks clarifying questions rather than guessing. In our deployment across the Kani and CBMC repositories, we have observed zero regressions introduced by the merged Kiro-generated code.

We started using Kiro in autonomous mode on the Kani repository in early November 2025 and expanded to CBMC later that month. Across both repositories, the numbers show the positive impact:

• Code maintenance (29%): Dependency updates, toolchain upgrades, CI improvements, and refactoring
• Documentation improvements (4%): Updates to project documentation and build instructions
• Bug fixes (36%): Resolution of reported issues, including crashes, incorrect results, and invariant violations
• Feature completion (26%): Addressing documented gaps in prototype features

The following chart shows monthly pull request activity in the CBMC repository. For most of 2025, the repository averaged fewer than 2 resolved issues per month. In November, that jumped to 60. Many of these pull requests are still working through review: of the 64 Kiro-submitted PRs in CBMC for November, 16 have been merged, 47 remain open, and 1 was closed because the underlying issue was resolved by another change, as of September 2026. Each one addresses a documented open issue. Across both CBMC and Kani, Kiro submitted pull requests addressing 87 unique issues in November and December 2025. In the prior 22 months (January 2024 through October 2025), the team addressed 94 issues total across both repositories.

Of the 94 pull requests Kiro submitted across CBMC and Kani in November and December 2025, as of September 2026, 35 (37%) have been merged, 56 (60%) remain open and under review, and 3 (3%) were closed because the underlying issues were resolved by other changes. Of the merged PRs, some were merged as submitted while others required interactive refinement. The review backlog reflects a key bottleneck: Kiro can generate PRs faster than the team can review them. These were substantial changes: the median PR touched 5 files and ~110 lines, while the largest touched about 1,000 files. At 2–3 hours of focused developer effort per task, the 94 PRs represent roughly 200–280 hours of implementation effort, excluding review time and PRs that may not ultimately merge; because many tasks involve bug fixes or feature completion rather than mechanical updates, this is best viewed as a lower bound.

The throughput shift is equally striking: CBMC averaged fewer than 2 resolved issues per month across the 22 months before Kiro, while November 2025 saw 60 resolved issues, a more than 30× increase. Nearly all of November’s 65 opened PRs (64) were Kiro-submitted, indicating that the spike reflects added agent capacity rather than redirected developer effort. Overall, Kiro generated implementation work at roughly 10× the team’s historical issue-resolution throughput, although realized value depends on review and refinement capacity. The merged PRs continue to introduce zero regressions, a signal that now rests on a much larger base: across the full deployment (November 2025 through September 2026), 183 Kiro-generated pull requests have been merged across the two repositories. The 56 still-open PRs from the initial cohort reflect the review bottleneck discussed above rather than quality concerns, and the zero-regression record will continue to be re-evaluated as they clear review.

The Kani project maintains a charon Git submodule to obtain an intermediate representation of Rust programs for alternative verification workflows. Unlike other submodules updated automatically through Dependabot, charon updates require integration testing because translation-layer changes can affect Kani’s ability to model Rust semantics correctly. A manual update typically takes 2–3 hours, covering the submodule update, compilation and build-failure investigation, upstream change analysis, regression testing, and test-failure investigation. Rather than repeatedly spending developer time on this work, we handed the process to Kiro, which handles it autonomously.

Kani issue #2236 had been in the backlog for over two years. Kani is an open-source formal verification tool for Rust, used in CI for critical AWS projects including Firecracker and s2n-quic, and relies on CBMC. A fuzzer had reported a Kani compiler crash with clear reproduction steps, but root-causing it required a substantial context switch. This is deliberate triage rather than neglect: issues that block users or threaten soundness are fixed immediately, while a fuzzer-found crash with no affected users loses the prioritization contest every time, it demands the same expensive context switch as a user-blocking bug, without the same payoff. After we added the kiro label, Kiro submitted PR #4461 with a fix and regression test in two hours and 22 minutes; human time spent was under five minutes. Because the issue was old, we asked Kiro to first verify whether the bug still existed, or, if resolved, add the reproduction case as a regression test. Kiro adapted its plan and produced a PR that we merged directly.

Kiro also produced PR #4445 and #4464, incrementally updating Kani’s charon Git submodule. Given only the instruction to make small, clearly described commits, Kiro analyzed available updates, determined the update sequence, generated the commits, and opened the PRs. Developers review the changes and can request work with /kiro fix for specific comments or /kiro all for all comments. The incremental commits and clear descriptions let reviewers focus on semantic correctness rather than mechanical update work.

The previous section gave the headline for Kani issue #2236: two years dormant, then resolved with under five minutes of human effort. Here is how the human-agent collaboration actually worked.

All it took was attaching the kiro label to the issue. The agent went to work, analyzing the issue and responding with a plan:

Given the issue was this old, it could very well have incidentally been fixed by some change. We responded to Kiro’s plan with the following guidance:

Kiro responded with an updated task plan, then produced the pull request that we merged as Kani PR #4461, with no context switch required from anyone on the team.

Understanding where Kiro failed was as important as its successes because it shaped work assignments and review expectations.

Incorrect fixes that pass CI. In CBMC PR #8892, a regression test used --no-library while calling memcpy, so the triggering code path was never exercised. The test passed with or without the fix. We replaced it with a unit test that directly exercised the affected function. Lesson: CI passing is necessary but not sufficient; reviewers must verify that tests validate the fix.

Architecturally wrong fixes. Some fixes addressed symptoms rather than root causes. In PR #8703, a 172-line restructuring broke nested quantifiers; the correct fix was 9 lines in the original location. These cases require reviewers with architectural knowledge, and Kiro also sometimes rebuilt functionality instead of using existing utilities.

Platform-specific failures. Because Kiro develops on Linux, platform issues can slip through. PR #8894 used empty structs (struct S {}), valid as a GCC extension but rejected in MSVC mode. The fix was adding a gcc-only tag, despite an existing test already demonstrating the relevant platform guard.

Formatting violations and stale PRs. Nearly every PR had minor formatting issues. Unreviewed PRs also accumulate conflicts: PR #7861 was 1,614 commits behind develop, requiring non-trivial rebasing. Prompt review is essential to avoid compounding costs.

The limitations described above were real, but they are not the end of the story. Every one of them was resolved without a developer opening an editor or IDE. Using Kiro CLI, maintainers start a kiro-cli chat session on the PR branch and guide fixes through conversation. The maintainer provides judgment; the agent provides execution. This two-phase workflow (autonomous generation, then interactive refinement) combines the strengths of both modes and keeps the total time cost well below a developer performing each task end-to-end.

Why two phases work. The autonomous agent eliminates the cold-start problem. By review time, there is working code, passing tests, and a clear approach description. The interactive CLI eliminates asynchronous back-and-forth latency, resolving issues in minutes instead of hours. Neither phase requires the maintainer to write code directly.

Qualitative impact. Rahul Kumar, Senior Manager of Applied Science in the AWS Automated Reasoning Group: “Kiro has fundamentally changed how we approach technical debt. Previously, submodule updates would sit in our backlog for weeks because they required context-switching from feature work. Now we label the issue with kiro and it handles the entire workflow, update, test, document. In November alone, we merged 15 Kiro-generated PRs into Kani with zero regressions.”

By handling routine maintenance, Kiro frees developers to focus on architectural decisions, complex algorithm design, community engagement, and research in formal verification.

If you want to try this on your own open-source project, follow the steps here.

For complex tasks or interactive refinement, use Kiro CLI on the pull request branch to guide the work through conversation, as described in the “Closing the loop” section above.

Kiro Web is generally available to all paid Kiro users at app.kiro.dev. If you are already a Kiro subscriber, sign in at app.kiro.dev/agent and follow the steps above.

As of September 2026, Kiro has submitted over 400 pull requests across the public CBMC and Kani repositories, of which 183 have been merged, addressing about 150 unique issues. In a private staging repository with over 430 flagged issues, it has produced over 360 additional pull requests being reviewed and upstreamed incrementally. If you maintain a repository with a backlog of well-defined issues, this approach will get you started in minutes.