Kiro

Your Code Has Bugs. Lean4 Has Proofs: Formal Verification for Engineers — Varun Pant, AWS

Aug 28, 2026 · 10:07

Varun Pant of AWS argues that formal verification is the only check that can prove AI-generated code correct for every input, as tests and human review cannot scale to the thousands of weekly pull requests coding agents now produce. He advocates spec-driven development with the Lean proof assistant, where humans own the specification and machines own the code and proof, validated by a small independent kernel. Pant walks through Lean's tactics via a chess analogy and details production examples: an AI rewrote zlib in Lean, generating 32,000 lines of proof; Cedar's Lean specification and Rust implementation are reconciled by roughly 100 million differential tests nightly; Verus uses Z3 solvers; and AWS's in-progress Starta tool aims to bring any language into the same verified core.

From AI-Assisted to AI-Native: Building a Frontier Development Team — Clare Liguori, AWS

Aug 28, 2026 · 20:57

Clare Liguori, Senior Principal Engineer at AWS, says Amazon's frontier development teams achieved step-function productivity gains by deliberately changing how they work with Kiro, its agentic coding assistant. In a 50-team pilot, half improved under 3x in deployment velocity and the other half hit a median 4.5x; the difference was habits, not tools. She defines frontier developers as writing 1-2% of their code, letting agents run for hours, and running multiple agents in parallel. The five habits: invest in agent context, slow down to speed up by refactoring brownfield codebases, feed agents specifications instead of babysitting them, make intent explicit, and shift testing left with deterministic mocks. She also warns that new bottlenecks emerge, like decision speed and burnout.

Using Spec-Driven Development for Production Workflows - Erik Hanchett, AWS

Jun 28, 2026 · 17:47

Erik Hanchett (AWS) argues that spec-driven development—writing markdown specification files before any code—produces higher quality code by guiding AI coding assistants, which he compares to 'AI interns' that need explicit direction. He introduces Kiro, AWS’s new AI IDE and CLI, which offers a spec mode that generates requirements documents, design documents with mermaid diagrams, property-based tests using Fastcheck, and a task list. In a demo building a movie website, Kiro created an MVP-focused implementation verified by property tests. Hanchett also highlights integrating external data via the Model Context Protocol (MCP) and stresses the importance of human review. He advises balancing context in steering docs and using on-demand skills to control the workflow.

Spec-Driven Development: Agentic Coding at FAANG Scale and Quality — Al Harris, Amazon Kiro

Jan 9, 2026 · 1:03:50

Al Harris, principal engineer at Amazon, presents Spec-Driven Development (SDD) with Kiro, an agentic IDE that transforms prompts into structured requirements (EARS format), designs, and property-based tests to ensure code correctness. He argues that upfront specification—augmented by MCP servers for external context—improves reproducibility and quality over pure vibe coding. The talk includes a live demo: building an S3-backed checkpointer for a LangGraph dad joke generator, then discovering Agent Core’s native memory is more idiomatic. Harris contrasts SDD with Cursor’s planning mode, explains how specs evolve as living documentation, and discusses handling session length, context pruning, and brownfield codebases. The result is a claim that spending 5–10 minutes on specs yields higher accuracy and reliable, testable outputs.