æ¬èšäºã¯ 2026 幎 11 æ 2 æ¥ã« Kiro ããã°ã§å
¬éãããã Kiro proves properties of its own harness in Lean ãã翻蚳ãããã®ã§ãã ç§ãã¡ã¯ãKiro ãèªèº«ã®ã³ãŒãã®äžéšã Lean ã§ã¢ãã«åãããã®ã¢ãã«ã«ã€ããŠã®å®çã蚌æããåã¢ãã«ã TypeScriptãRustãPython ã®ã³ãŒããšç
§ããåãããäœæ¥ããèªåã§é²ããä»çµã¿ãäœããŸãããæåã«é©çšãã察象㯠Kiro èªèº«ã§ãã26 åã®é¢æ°ã®ã¢ãã«ã«ã€ããŠãæ§è³ªã®åè£ãšèгå¯ãåãã㊠96 ä»¶ãåæããŸããããã®ãã¡ 70 件㯠Lean ã§èšŒæã§ãã2 ä»¶ã¯æçæ€æ»ïŒäžéãŸã§ã®æéã®å
¥åã調ã¹ãæ€æ»ïŒãè¡ããŸããã18 ä»¶ã¯ã¢ãã«ã®äžã§å蚌ãããåæå¯Ÿè±¡ã®ã³ãŒãã§ãåçŸã§ããŸãããæ®ãã® 6 ä»¶ã¯éšåçãªçµæã芳å¯ã§ããæ¬èšäºã§ã¯ãLean ã䜿ã£ãæ€èšŒã®ã¯ãŒã¯ãããŒããå®éã«æ¬çªã§äœ¿ãããŠãããšãŒãžã§ã³ãã®ããŒãã¹ã«ã€ããŠããã®æ§è³ªãæ€èšŒããé ãããã°ãèŠã€ããã®ã«äœ¿ããããšã瀺ããŸãã ç§ãã¡ã®ããŒã 㯠Kiro ã®ã³ã³ããã¹ã管çãæ
åœããŠããŸããLLM ãåãå·»ãããŒãã¹ã¯ãäœãã©ãã ãã³ã³ããã¹ããŠã£ã³ããŠã«å
¥ããããæ±ºããé·ãäŒè©±ãå§çž®ããããã³ãããã£ãã·ã¥ãå¹ãããã«åãªã¯ãšã¹ãã®ãã¬ãã£ãã¯ã¹ïŒå
é éšåïŒãå®å®ãããã»ãã·ã§ã³ã埩å
ã§ããããã«ä¿åããŸãããã®åšãã«ã¯ãããŒã«åŒã³åºããšãã®æ¿èªãã¹ããªãŒãã³ã°ã®å¿çããµããšãŒãžã§ã³ããããã¯ã°ã©ãŠã³ãã¿ã¹ã¯ãšãã£ããããŒãã¹ã®ã»ãã®åºæ¬æ©èœããããŸãããã®ã³ãŒãã®ãã°ã¯ãã¹ãã§èŠã€ãã«ãããã®ã§ãããã°ãåºããã©ããã¯ãLLM ãéžã¶å
¥åã䞊è¡ããã€ãã³ãã®é åºãå€ãã®ã¿ãŒã³ãåèµ·åãçµãŠç©ã¿äžãã£ãç¶æ
ã«å·Šå³ãããŸãããããããããããã°ã¯ãšã©ãŒãåºããã«èµ·ããããšãå€ããLLM ã¯å°ãã ã誀ã£ãã³ã³ããã¹ãã®ãŸãŸäœæ¥ãç¶ããŸããããã§ç§ãã¡ã¯ããã®åºç€ãæ·±ã調ã¹ãŠãã°ãèŠã€ããæ¹åã«ã€ãªããèªååã®æ¹æ³ãæ¢ããŠããŸãã Kiro ãèªèº«ã®ããŒãã¹ã確ãããæ¹æ³ã ç§ãã¡ã¯ Kiro ã«ãèªèº«ã®ããŒãã¹ã«ãã 26 åã®é¢æ°ã®æ§è³ªã蚌æããããé Œã¿ãŸããããšãŒãžã§ã³ãã¯å颿°ããããã°ã©ãã³ã°èšèªã§ããèšŒææ¯æŽç³»ã§ããã Lean 4 ã§ã¢ãã«åããåã¢ãã«ãå®éã®ã³ãŒããšç
§ããåãããããã§ãæåŸ
ãããæ¯ãèããæãç«ã€ããšã蚌æãããããããç Žãå
¥åãïŒLean ã®åäŸãšããŠïŒèŠã€ããŸããã察象㯠Kiro ã® 3 ã€ã®ã³ãŒãããŒã¹ïŒKiro ãšãŒãžã§ã³ãããŒãã¹ãCLI ã¯ã©ã€ã¢ã³ããKiro CrewïŒã§ããKiro CLI ã«ã³ãŒãããŒã¹ãèµ°æ»ãããLean ã®ã¢ãã«ãäœããçšåºŠã«å°ããããã€ãã¹ãããã®ãç°¡åã§ã¯ãªã颿°ã察象ãšããŠéžã°ããã®ã§ãã©ãã調ã¹ã䟡å€ã®ãã察象ã§ããããã¯ãèªåãåããŠããã·ã¹ãã ãæ¹åãããšãŒãžã§ã³ãã«åããŠããŸã å§ãŸã£ãã°ããã®åãçµã¿ã§ãããã¹ãŠã®èšŒæã¯ Lean ã®ã«ãŒãã«ïŒèšŒæãæ£ããããæçµçã«æ€æ»ãããLean ã®å°ããªäžæ žéšåïŒãæ€æ»ãããã¹ãŠã®çºèŠã¯å®éã®ã³ãŒãã§ç¢ºããããã¹ãŠã®å®çã®èšè¿°ã¯ç§ãã¡ãã¬ãã¥ãŒããŸããããœãŒã¹ã³ãŒããšããã蚌æã§ããã«ãŒãã«ã®æ€æ»ã¯éã£ãŠããŸãããã§ããããããŠã§ããã®ã¯ãããã³ãããã£ãã·ã¥ã®ä¿èšŒã䞊è¡åŠçã®ããã«ããã¹ãã§ã¯æ€èšŒãå±ãã«ããéšåãè£ããç¹°ãè¿ã䜿ããæé ã§ããLean ã®ã«ãŒãã«ãéã£ã蚌æã¯ãåäœãã¹ãã«ããæéåã®å
¥åã ãã§ãªããã¢ãã«åãããã¹ãŠã®å
¥åã«ã€ããŠä¿èšŒãäžããŸãã蚌æã«å€±æããå Žåã¯ãå®éã®ã³ãŒãã§è©Šããå
·äœçãªåäŸãèŠã€ããããšããããŸãã 蚌æããããšã Kiro ãšãŒãžã§ã³ããµãŒããŒïŒKiro ããŒãã¹ãšãåŒã³ãŸãïŒãKiro CLI v3ãKiro Crew ã®äžæ žã«ãã 26 åã®é¢æ°ã«ã€ããŠãLean ã¯ãããã®ã¢ãã«ã«é¢ãã 70 åã®æ§è³ªã蚌æããŸãããã©ã®æ§è³ªããå®çã«æžããä»®å®ãæºãããã¢ãã«åãããã¹ãŠã®å
¥åã«ã€ããŠæãç«ã¡ãŸããåã¢ãã«ã¯ãã©ã³ãã ã«çæããå
¥åã§å®éã®ã³ãŒããšç
§ããåãããŠããŸãïŒãææ³ããšãå¶çŽãã®ç¯ãåç
§ïŒãããšãã°æ¬¡ã®ããšã蚌æããŸããã éè€ãããã¡ã€ã«æ·»ä»ãåãé€ããŠããåã®ã¿ãŒã³ã§ LLM ãèŠãå
容ã¯å€ãããŸããããã®ãããäŒè©±ãé·ããªã£ãŠãããã®åŠçãããã³ãããã£ãã·ã¥ã®ãã¬ãã£ãã¯ã¹ãå£ãããšã¯ãããŸããã ãµããšãŒãžã§ã³ãã®æš©éã®å€å®ã芪ã®å€å®ãšçµã¿åãããŠãã芪ãã倧ããªæš©éã«ã¯ãªããŸããããŸããããªã·ãŒãå³ããããŠããæåŠãæ¿èªã«å€ããããšã¯ãããŸããã Kiro Crew ã®ãã¥ãŒã«ããã¿ã¹ã¯ãæ°ããã¯ãŒã«ãŒã«æž¡ã£ãããšã¯ãå€ãã¯ãŒã«ãŒã®ãã§ã³ã¹ä»ãã®æžã蟌ã¿ïŒååŸãããšãã®äžä»£çªå·ãæ·»ããæžã蟌ã¿ïŒã§ãã®ã¿ã¹ã¯ãå€ããããšã¯ãããŸããããã ããã¹ãã¢ã®ååŒã³åºããäžå¯åãªïŒã¢ãããã¯ãªïŒ1 ã¹ããããšããŠå®è¡ãããããšãåæãšããŸãã èŠã€ãã£ãããšã 蚌æã倱æããç®æããã¯ããã¹ããå±ããŠããªãã£ããšããžã±ãŒã¹ãèŠã€ããããšããããããŸãããå€ã㯠2 ã€ã®è¡šçŸã®å¢ç®ã 2 ã€ã®ããã°ã©ã ã®å¢ç®ããããã¯äžŠè¡ããã€ãã³ãã®ãŸããªé åºã«ãããŸããã倱æãã蚌æãçºèŠãšããŠæ°ããã®ã¯ãæãå ããŠããªãå®éã®ã³ãŒãã§åçŸã§ãããã®ã ãã§ãã ãšãŒãžã§ã³ãã«ãã¹ãã ãã§ã¯è¶³ããªãçç± éåžžã®ãã¹ãã¹ã€ãŒãã¯ãäººãæžãããã®ã§ã LLM ãçæãããã®ã§ãã誰ããæãã€ããå
¥åãçæåšãäœã£ãå
¥åã確ãããã ãã§ããã¹ãŠã®ã³ãŒããŒã±ãŒã¹ã¯æããããŸããããšãŒãžã§ã³ãã§ã¯ãå
¥åã®å€§å㯠LLM ãš LLM ãèªããã¡ã€ã«ããæ¥ããããå
¥åããšãããã±ãŒã¹ã¯ã誰ãããã¹ãã«æžãæ°ããã¯ããã«å€ããªããŸãããããæ±ãã³ãŒãã¯å°ãããèŠãããã«æ£ããããªããšããããããŸããåãè©°ããèªã¿åãå°çšãã©ããã®å€å®ãèš±å¯ãªã¹ããšã®ç
§åãªã©ã§ãã蚌æããã£ãšã圹ã«ç«ã€ã®ã¯ããããç®æã§ãããããã颿°ã¯æ£ç¢ºã«ã¢ãã«åã§ããã»ã©çããã³ãŒãã®æå³ã¯å®çãšããŠæžããã»ã©æç¢ºã§ãããããã¹ãŠã®ã»ãã·ã§ã³ã§å®è¡ãããŸããç¶²çŸ
çã§ãªãéåžžã®ãã¹ãã¹ã€ãŒãã¯æ¯ãèããæšæ¬ãšããŠç¢ºãããã ãã§ããã蚌æã¯åœ¢åŒã¢ãã«ã«ã€ããŠããã¹ãŠã®å Žåã«æãç«ã€çµæã瀺ããŸãããã ãã蚌æã察象ãšããã®ã¯ãããŸã§ã¢ãã«ãªã®ã§ãåŸã§èª¬æããããã«ãã¢ãã«ãšã³ãŒããçµã³ä»ãããã¹ãã¯åŒãç¶ãå¿
èŠã§ãã ãšãŒãžã§ã³ããµãŒããŒãCLIãKiro Crew ã®ã©ãã§ããããŒãã¹ã¯æ¬¡ã®ãããªçš®é¡ã®æ§è³ªã®äžã«æãç«ã£ãŠããŸããç¶²çŸ
çã§ãªããã¹ãã§ã¯ãã©ããæšæ¬ãšããŠç¢ºãããããšããã§ããŸããã å
容ã®äžéã LLM ã®ã³ã³ããã¹ããŠã£ã³ããŠã«å
¥ãå
容ã«ã¯ãã©ãããµã€ãºã®äžéããããŸããå
容ãåãè©°ããããå ŽåããšãŒãžã§ã³ãã¯æ®ããååŸã§ããŸãã æ°žç¶åã åèµ·åããããšã§ããã»ãã·ã§ã³ãèªã¿èŸŒã¿çŽããšãLLM ã«ã¯ãã»ãã·ã§ã³ãç¶ããŠãããšãã«èŠãŠããã®ãšãŸã£ããåãã¡ãã»ãŒãžãæž¡ããŸãã ããã³ãããã£ãã·ã¥ã åãªã¯ãšã¹ãã®ãã¬ãã£ãã¯ã¹ïŒããŒã«ã®äžèЧãæåã®ã¡ãã»ãŒãžãå±¥æŽïŒãã¿ãŒã³ããŸããã§å€ãããªãã®ã§ãLLM ã®ãããã€ããŒã¯ãã£ãã·ã¥ããåŠçãåå©çšã§ããŸãã æš©éã æ¿èªã¯ãæ¿èªããç¯å²ã ãã«ãã£ã¡ãå¹ããŸãããŸãããµããšãŒãžã§ã³ãã芪ãã倧ããªæš©éãæã€ããšã¯ãããŸããã é åºã ã»ãã·ã§ã³ãã¹ããªãŒãã³ã°ã®å¿çãããã¯ã°ã©ãŠã³ãã¿ã¹ã¯ã¯ãã€ãã³ããã©ã®é åºã§å±ããŠãæ£ããç¶æ
ã§çµãããŸãã ãªããžããªããŸããå¥çŽã 2 ã€ã®ã³ãŒãããŒã¹ãäºãã«äŸåããŠããç®æã§ã¯ãäž¡è
ã®ããã ã®çŽæäºïŒå¥çŽïŒãå®ãããŠããå¿
èŠããããŸããããšãã° Crew ã¯ãããŒã«ã®èš±å¯ãªã¹ã 1 ã€ãããšãŒãžã§ã³ããµãŒããŒåããš CLI åãã®äž¡æ¹ã®åœ¢åŒã«å€æããŸãããŸã CLI ã¯ãã»ãã·ã§ã³ã®éå§æã«ãšãŒãžã§ã³ããµãŒããŒããå±ãæŽæ°ãåãããŒããŠã¯ãããŸãããåãªããžããªã®ãã¹ãã確ãããã®ã¯ãéåžžã¯èªåã®ãªããžããªã®ã³ãŒãã ãã§ããLean ã®ã¢ãã«ãªãäž¡åŽãå«ããŠãäž¡è
ãäžèŽããããšã蚌æã§ããŸãã ã©ããããã¹ãŠã®å
¥åããã¹ãŠã®ã»ãã·ã§ã³ããããã¯ã€ãã³ãã®ãã¹ãŠã®é åºã«ã€ããŠã®åœé¡ã§ããããã¯ãŸãã«å®çãšããŠæžã圢ã®åœé¡ã§ãç¶²çŸ
çã§ãªããã¹ãã§ã¯æšæ¬ãšããŠç¢ºãããããšããã§ããªã圢ã§ãã ææ³ äœæ¥ã¯ Kiro èªèº«ãè¡ããŸãããå
·äœçã«ã¯ãKiro CLI ã Amazon Bedrock ã§æäŸããã Claude Opus 5.5 ã䜿ããLean 4 çšã®äžé£ã®ã¹ãã«ãèªã¿èŸŒãã§äœæ¥ããŸããããšãŒãžã§ã³ãã¯å¯Ÿè±¡ãèŠã€ããLean ã®ã¢ãã«ã蚌æãå·®åãã¹ãïŒåãå
¥åãã¢ãã«ãšå®éã®ã³ãŒãã«äžããŠåºåãæ¯ã¹ããã¹ãïŒãåçŸã¹ã¯ãªãããæžããŸãããåçŸã¹ã¯ãªããã¯ãæãå ããŠããªãå®éã®ã³ãŒãã«å¯ŸããŠåäŸãå®è¡ããå°ããªããã°ã©ã ã§ããçæããã蚌æã¯ããšãŒãžã§ã³ããšã¯ç¬ç«ã« Lean ãæ€æ»ããŸãããã ãããã®èšŒæãæ¬çªã®ã³ãŒãã«çµã³ä»ãããããã©ããã¯ãã¢ãã«ãå®çã®èšè¿°ãå·®åãã¹ãã®å®è¡ç°å¢ïŒãã¹ãããŒãã¹ïŒã®æ£ç¢ºãã«ããã£ãŠããããããã¯ç§ãã¡ãå¥ã«ã¬ãã¥ãŒããŠãã¹ãããŸãããç¯å²ã決ããã®ã¯ç§ãã¡ã§ã察象ã®ãªããžããªãšé åãéžã³ãå®çã®èšè¿°ãšçºèŠãäžãã£ãŠãããã³ã«ã¬ãã¥ãŒããŸãããåå®çã¯ãã³ãŒãã®æå³ã圢åŒçãªåœé¡ãšããŠæžãçŽãããã®ã§ãïŒã³ãŒãã®æå³ã¯ããã¥ã¡ã³ããèšèšäžã®äžå€æ¡ä»¶ããå°ããçºèŠã¯ãã¹ãŠå®éã®ã³ãŒãã§ç¢ºèªããŠããŸãïŒã䜿ã£ãã®ã¯ Lean 4.28.0 ã®ãã£ã¹ããªãã¥ãŒã·ã§ã³ã ãã§ãMathlibïŒLean ã®æ°åŠã©ã€ãã©ãªïŒã®ãããªãLakeïŒLean ã®ãã«ãããŒã«ïŒã§åã蟌ãå€éšã®äŸåã¯äœ¿ã£ãŠããŸããããšãŒãžã§ã³ããµãŒããŒã¯ Kiro ã® IDEãWebãCLI v3 ãå
±æããããŒãã¹ã§ïŒã One agent, every surface ãïŒãCLI ã«ã€ããŠã®çµæã¯ Kiro CLI v3 ã«åœãŠã¯ãŸããŸãããšãŒãžã§ã³ããµãŒããŒãš Kiro CLI ã¯ããããã®éå
¬éãªããžããªã§ãKiro Crew ã¯å
¬éãªããžããªã®ã³ããã 909e0fc ã§åæããŸãããæ¬èšäºã®æ°åã¯ãKiro ããŒã ãã¬ãã¥ãŒãã瀟å
ã®å®éšçµæã§ãã 蚌æãæžããã®ããšãŒãžã§ã³ããªã®ã§ãæå³ã¯è¿ããã®ã®ã³ãŒãã®æå³ãæãèœã¡ããŽãŒã«ïŒèšŒæãã¹ãåœé¡ïŒã Lean ãåãå
¥ããŠããŸãã±ãŒã¹ããªããã確ãããŸãããå
·äœçã«ã¯ãæªå®æã®ã¹ããããäœåãªå
¬çãæ±ºããŠåæã«ã¯æãç«ããªãä»®å®ããªããã調ã¹ãŸããããã¹ãŠã®å®çã5 ä»¶ã®çºèŠãè£ä»ãã 10 åã®åäŸããã®ãã¡ 1 ä»¶ã®çºèŠã®ããã® 1 ã€ã®å¯Ÿç
§ã±ãŒã¹ã«ã€ããŠããããããäŸæ ããå
¬çãæŽãåºããŸãããä»®å®ã©ãããççŸããå®çã¯èªæã«æãç«ã€ïŒç©ºèã«çã«ãªãïŒã®ã§ã圹ã«ç«ã¡ãŸãããæ¬èšäºã§åŒçšãŸãã¯èª¬æããå®çã®ãã¹ãŠã«ã€ããŠãä»®å®ããã¹ãŠæºããå
·äœçãªå
¥åãäžã㊠Lean ã§æ€æ»ããåå®çã®ä»®å®ãåæã«æºãããããšã確ãããŸããã Lean ã¢ãã«ãšã¯ Lean ã¢ãã«ãšã¯ã颿°ãããäžåºŠ Lean ã§å®è£
ãããã®ã§ãããœãŒã¹ã®å
¥åãšèŠ³æž¬ã§ããåºåãæç€ºçãªãšã³ã³ãŒãã£ã³ã°ã§è¡šããLean ãæšè«ã§ããããã«æžããŸããå®çã察象ãšããã®ã¯ã¢ãã«ã§ããœãŒã¹ã³ãŒãã§ã¯ãããŸãããLean 㯠Python ã TypeScript ã Rust ãèªããªãããã§ãããããã£ãŠã¢ãã«ã¯ããã®ãšã³ã³ãŒãã£ã³ã°ã®ããšã§ãœãŒã¹ãšåããã®ãèšç®ãããªããã€æ§è³ªã蚌æã§ããã»ã©åçŽã§ãªããã°ãªããŸããã 䞊è¡åŠçã®åé¡ãèµ·ãããããKiro Crew ã®ã¿ã¹ã¯ãã¥ãŒã®äŸãèŠãŠã¿ãŸãããã¥ãŒã¯ SQLite ã«ã¿ã¹ã¯ããšã« 1 è¡ãæã¡ã倿°ã®ãã£ã¹ãããã£ãŒïŒãã¥ãŒããã¿ã¹ã¯ãåã£ãŠã¯ãŒã«ãŒã«æž¡ãåŠçïŒãå®è¡ã«ãŒããã³ãŒã«ããã¯ãåæã«ãã¥ãŒãåŒã³åºããŸãã2 ã€ã®ãã£ã¹ãããã£ãŒãåãã¿ã¹ã¯ãåæã«åãããšããããšããããåãŠãã®ã¯çæ¹ã ãã§ãããããæ±ºããã®ã claim ã§ãã¹ãã¢ã®ããã¯ã®ããšããã©ã³ã¶ã¯ã·ã§ã³ã®äžã§ãæ¡ä»¶ä»ãã® UPDATE ã 1 åå®è¡ããŸãã taskq/store.py ã«ãããã®äžå¿éšåã¯æ¬¡ã®ãšããã§ãã with self._lock: conn = self._c() try: conn.execute("BEGIN IMMEDIATE") cur = conn.execute( "UPDATE tasks SET state=?, lease_owner=?, lease_expires_at=?, " "generation=generation+1, attempts=attempts+1, next_run_at=NULL, " "updated_at=? " f"WHERE id=? AND state IN {_SQL_CLAIMABLE} " "AND (next_run_at IS NULL OR next_run_at<=?) " "AND (lease_expires_at IS NULL OR lease_expires_at<?)", (ADMITTED, who, ts + lease, ts, task_id, ts, ts), ) if cur.rowcount != 1: conn.execute("COMMIT") return None row = conn.execute("SELECT * FROM tasks WHERE id=?", (task_id,)).fetchone() rec = TaskRecord.from_row(row) self._append_event_in_tx( conn, task_id, "claimed", {"owner": who, "generation": rec.generation} ) conn.execute("COMMIT") except sqlite3.Error as exc: self._rollback(conn) raise TaskStoreUnavailable(f"task claim failed: {exc}") from exc return ClaimResult(record=rec) ããã«å¯Ÿå¿ãã Lean ã¢ãã«ã¯æ¬¡ã®ãšããã§ãã /-- The columns the write paths read or set. Owner 0 is the store's own incarnation. -/ structure Row where state : St gen : Nat attempts : Nat owner : Option Nat expires : Option Nat nextRun : Option Nat hasWait : Bool /-- `claim` (store.py:877): one UPDATE guarded by state, `next_run_at` and lease. -/ def claim (who now lease : Nat) (r : Row) : Option Row := if claimable r.state && r.nextRun.all (· †now) && r.expires.all (· < now) then some { r with state := admitted, gen := r.gen + 1, attempts := r.attempts + 1, owner := some who, expires := some (now + lease), nextRun := none } else none å¿é
ãªã®ã¯ãã¿ã¹ã¯ã 2 åå®è¡ãããããšã§ãã2 ã€ã®ãã£ã¹ãããã£ãŒããã¥ãŒã§åŸ
ã£ãŠããåãã¿ã¹ã¯ãåæã«èŠãŠãã©ã¡ãã claim ãåŒãã§åãã«ããããšããããŸããäž¡æ¹ã®åŒã³åºããæåãããšã2 ã€ã®ãšãŒãžã§ã³ããåãäœæ¥ãããã¿ã¹ã¯ã Kiro ã®å€ã§å€ãããã®ã¯ãã¹ãŠ 2 åå€ãã£ãŠããŸããŸããæ¬¡ã® Lean ã®å®çã¯ããããèµ·ããªãããšã瀺ããŸãããããã£ã¹ãããã£ãŒã® claim åŒã³åºããæåããçŽåŸãã¿ã¹ã¯ã¯ admitted ïŒååŸæžã¿ã§ãããããéå§ããç¶æ
ïŒã«ãªããã»ãã®ã©ã®ãã£ã¹ãããã£ãŒããã® claim åŒã³åºããããã€è¡ãããŠãæåŠãããããšããå
容ã§ããã¿ã¹ã¯ãåã³åããããã«ãªãã®ã¯ããªãã©ã€ã®äºçŽã®ããã«ãã¿ã¹ã¯ããã¥ãŒã«æ»ãæžã蟌ã¿ãããšã§è¡ããããšãã ãã§ãã theorem claim_exclusive (who who' now now' lease : Nat) (r r' : Row) (h : claim who now lease r = some r') : claim who' now' lease r' = none â§ r'.state = admitted ãã®å®çã¯ãããŠå°ããããŠãããŸãã claim ã®æ¡ä»¶ãšã admitted ãååŸå¯èœãªç¶æ
ã§ã¯ãªãããšããå°ãããŸãããã®å®çã®äŸ¡å€ã¯ãäŸæ ããŠããæ¡ä»¶ããå·®åãã¹ãã§å®éã® SQL ãšäžèŽããããšã確ãããæ¡ä»¶ãã®ãã®ã§ããç¹ã«ãããŸãã蚌æã®é£ããã«äŸ¡å€ãããããã§ã¯ãããŸããããã®å®çãè¿°ã¹ãã®ã¯ claim ãæåããçŽåŸã®è¡ã«ã€ããŠã§ããã®åŸã®åŒã³åºãããŸããã§äœãèµ·ãããã¯ãåŸã§ç޹ä»ãã stale_writer_fenced_out ãæ±ããŸãã䞊è¡åŠçã«ã€ããŠã¯ãæåãããã©ã³ã¶ã¯ã·ã§ã³ã¯ãããã 1 ã€ã®äžå¯åãªç¶æ
é·ç§»ã§ããããšããä»®å®ãéããŠããæ±ã£ãŠããŸããããã®ä»®å®ã®ããšã§ã¯ãååŸå¯èœãªåãè¡ã«å¯Ÿã㊠2 ã€ã® claim åŒã³åºããã©ã¡ããæåããããšã¯ãããŸãããç«¶åããæ¥ç¶ã¯ã代ããã«ããã¯ã®ãšã©ãŒãåãåãããšããããŸãã BEGIN IMMEDIATE ã¯ã¹ãã¢ã® busy_timeout ãŸã§åŸ
ã£ãŠãã倱æãã claim 㯠TaskStoreUnavailable ãéåºããŸãããªãã©ã€ãå¯çšæ§ããã®ãšã©ãŒã®çµè·¯ã¯ãã®å®çã®ç¯å²å€ã§ããCrew ã®ã²ãŒããŠã§ã€ïŒKiro Crew ã®åžžé§ããã»ã¹ïŒã¯èªåã®ããŒã ãã£ã¬ã¯ããªã«ãã¡ã€ã«ããã¯ããããã®ã§ã2 ã€ç®ã®ã²ãŒããŠã§ã€ãåãããŒã¿ããŒã¹ã«æžã蟌ãããšã¯ã§ããŸãããããã§ããæåã® sqlite3 ã»ãã·ã§ã³ã®ãããªå¥ã®ããã»ã¹ãªãæžã蟌ããŠããŸããŸããããã»ã¹ããŸããã äžå¯åæ§ãä¿èšŒããŠããã®ã¯ SQLite ã®æžã蟌ã¿ããã¯ã ãã§ããã®åæã¯ Lean ã§ã¯æ€æ»ããŠããŸããã ã¢ãã«ã¯ããã€ãã®ç¹ã§ãœãŒã¹ãšç°ãªããŸããã¢ãã«ã¯çŽç²é¢æ°ã§ãç¶æ
ãåãåã£ãŠæ°ããç¶æ
ãè¿ããŸããã¢ãã«ã¯åŒã³åºãã®åãæ±ããã¹ãã¢ã®åæäœãäžå¯å㪠1 ã¹ããããšããŠæ±ããŸããããã¯ã¹ãã¢ã«ã€ããŠã®ä»®å®ã§ãLean ã蚌æãããã®ã§ã¯ãããŸãããããã»ã¹å
ã§ã¯ã¹ãã¢ã®ããã¯ã«ãããã»ã¹éã§ã¯ SQLite ã®ãã©ã³ã¶ã¯ã·ã§ã³ã«äŸæ ããŠããŸããæå»ãæååã®ãšã³ã³ãŒãã£ã³ã°ããã€ãæ°ã®äžéã®ããã«ããã°ãæœã¿ããç®æã§ã¯ããŒã¿ãæ£ç¢ºã«è¡šããŠããŸãããŸããã¢ãã«ã¯æ®éã®ããã°ã©ã ã«ã³ã³ãã€ã«ã§ããã®ã§ãå®éã®ã³ãŒããšäžŠã¹ãŠå®è¡ã§ããŸãã ã¢ãã«ã圹ã«ç«ã€ã®ã¯ããœãŒã¹ã³ãŒããšåãããšãããå Žåã ãã§ããåã¢ãã«ã®åé ã«ã¯å
ã®ãœãŒã¹ãã¡ã€ã«ãšè¡çªå·ã瀺ãããããŒããããã¬ãã¥ã¢ãŒã 2 ã€ã䞊ã¹ãŠæ¯ã¹ãããããã«ããŠããŸãããã®ã¬ãã¥ãŒã ãã«ã¯é Œã£ãŠããŸãããã©ã®ã¢ãã«ãæ°ååã®ã©ã³ãã ãªå
¥åã§å®éã®ã³ãŒããšäžŠã¹ãŠå®è¡ããåºåã®éãããªããªããŸã§ã¢ãã«ãçŽããŸããïŒåŸè¿°ã®æé 3ïŒããã®ããã§å®çã¯ãä»®å®ãæºããã¢ãã«åãããã¹ãŠã®å
¥åã«ã€ããŠãã¢ãã«ã®äžã§æãç«ã¡ãŸããå·®åãã¹ãã¯ã¢ãã«ãšãœãŒã¹ãäžèŽããããšã®èšŒæ ã§ãã£ãŠã蚌æã§ã¯ãããŸããã詊ãããã¹ãŠã®å
¥åã§äžèŽããããšã瀺ãã ãã§ãã©ããŸã§ä¿¡é Œã§ãããã¯ãçæããå
¥åãå£ããããã±ãŒã¹ãã©ãã ãçªããŠãããã§æ±ºãŸããŸãã ããã«ã¯ããã®çš®ã®ææ³ã§ããåé¡ã«ãªããã¢ãã«ãšã³ãŒãã®ããéãæ®ããŸãã蚌æã¯ä»®å®ãæºããã¢ãã«åãããã¹ãŠã®å
¥åã察象ãšããäžæ¹ãã¢ãã«ãšã³ãŒãã®äžèŽã¯çŽ 100,000 åã®ã©ã³ãã ã«çæããå
¥åã§ãã確ãããŠããŸãããããã§ã¯ 3 ã€ã®ããšããã®ããéãå°ããä¿ã£ãŠããŸãã颿°ãçãããšãã¢ãã«ããœãŒã¹ã³ãŒãã®æ§é ãä¿ã£ãŠããããšããããŠçæåšãããã«ããã€ãã®ããã¹ããäžéã¡ããã©ã®é·ããé åºãå
¥ãæ¿ããã€ãã³ãã®ããã«ããããã®é¢æ°ãå£ããããå
¥åãçã£ãŠããããšã§ãããã¹ãèªäœã®ç¢ºèªãšããŠã2 ã€ã®ãã©ãã«ãŒã«ã€ããŠå®éã®ã³ãŒãåŽã®æ¯ãèãã 1 ã€å€ããŠã¿ããšãããå·®åãã¹ãã¯æ°çŸä»¶ã®äžäžèŽãå ±åããŸããã ã©ã®ãªããžããªã§ãåãæé ãèžã¿ãŸãããå³ 1 ã«å
šäœã®æµãã瀺ããŸããäžäžèŽãåºããšãã«ã¢ãã«ã®ä¿®æ£ã«æ»ã 2 ãæãå«ããŠããŸãã å³ 1: æ€èšŒã®æµãããªã¬ã³ãžã®æé 㯠Kiro CLI ã®ãšãŒãžã§ã³ããè¡ããçŽ«ã®æé 㯠Lean ã®äžã§è¡ããéã®æé ã§ã¯å®éã®ã³ãŒããå®è¡ããŸããç Žç·ã¯ãã¢ãã«ãã³ãŒããšäžèŽããæé 2 ã«æ»ãããšã衚ããŸãã 1. 察象ãèŠã€ããã åãªããžããªïŒKiro ããŒãã¹ãKiro CLIãKiro CrewïŒã Kiro CLI ã«èªãŸããã³ãŒãã«ã€ããŠã®åœé¡ãå®çãšããŠæžãã颿°ãæ¢ãããé Œã¿ãŸããããµã€ãºã®äžéãæ¿èªã®ã«ãŒã«ãã©ã€ãã®ã»ãã·ã§ã³ïŒåèµ·åããã«ç¶ããŠããã»ãã·ã§ã³ïŒãšäžèŽããªããã°ãªããªãåèªã¿èŸŒã¿ã決ããŠåŸæ»ãããŠã¯ãããªãã¹ããŒããã·ã³ãªã©ã§ããèµ°æ»ã§ã¯ããã¥ã¡ã³ãã³ã¡ã³ããèšèšäžã®äžå€æ¡ä»¶ãåŒã³åºãç®æãèªã¿ãå察象ã®ãœãŒã¹ãã¡ã€ã«ãšè¡ãä»ãããåªå
é äœä»ãã®å¯Ÿè±¡ã®äžèЧãäœããŸãããã¢ãã«ã¯ã³ãŒããäœãããããèšè¿°ããå®çã¯ã³ãŒããæºããã¹ãæ¯ãèããè¿°ã¹ãŸãã 2. ã¢ãã«åããã ãšãŒãžã§ã³ãã¯åè¿°ã®ãšããå颿°ã® Lean ã¢ãã«ãæžããŸãããã¬ãã¥ã¢ãŒã 1 è¡ãã€æ¯ã¹ãããããã«ãå
ã®ã³ãŒãã®æ§é ãä¿ã£ãŠããŸãã 3. ã¢ãã«ãå®éã®ã³ãŒããšç
§ããåãããã ã¢ãã«ã誀ã£ãŠããã°ãããã«ã€ããŠèšŒæããŠãå®éã®ã³ãŒãã«ã€ããŠã¯äœãèšããŸãããããã§ãäœãã蚌æããåã«ãå Lean ã¢ãã«ãå®è¡ãã¡ã€ã«ã«ã³ã³ãã€ã«ããæ°ååã®ã©ã³ãã ãªå
¥åã§å®éã®å®è£
ãšäžŠã¹ãŠå®è¡ããŸãããTypeScript 㯠Node ã Bun ã§ãRust ã¯å®éã®ã¯ã¬ãŒãã«ãªã³ã¯ããå°ããªãã€ããªã§ãPython ã¯å®éã®ã¢ãžã¥ãŒã«ã import ããŠå®è¡ããŸããå
¥åã¯ãã©ã³ãã ãªæååãã©ã³ãã ãªåŒã³åºãã®åãããå®éã® bash ãš git ã§å®è¡ããã·ã§ã«ã³ãã³ããŸã§ãããŸãããçæåšã¯å¢çãçããŸããããã«ããã€ãã CJK ã®ããã¹ããåäžéã®ããäžãšããäžã®é·ããã·ã£ããã«ãããç¹°ãè¿ãããããã€ãã³ãã®é åºãCLI ãã»ãã·ã§ã³éå§æã«ä¿çããæŽæ°ã®äžé 64 ä»¶ãè¶
ãã倧éã®æŽæ°ãªã©ã§ããåºåãéã£ããšãã¯ã©ã¡ãã誀ã£ãŠãããã確ãããã¢ãã«åŽã誀ã£ãŠããã°ã¢ãã«ãçŽããŸããã3 ã€ã®ã³ãŒãããŒã¹ã§åèš 97,938 ã±ãŒã¹ãæµããæçµã®å®è¡ã§ã¯ãäžäžèŽã¯ãããŸããã§ããã 4. 蚌æããã 察象ã®ã³ãŒãã®æå³ãããããå®çãšããŠæžãã蚌æããŸããã蚌æãè¡ãè©°ãŸãçç±ã¯ããã€ãèããããŸããå®çãåœãªã®ãããããŸããããã¢ãã«ã誀ã£ãŠããã®ãããããŸãããã蚌æãæªå®æãªã®ãããããŸãããè¡ãè©°ãŸã£ã蚌æã¯ 1 ã€ãã€èª¿ã¹ãŸãããè¡ãè©°ãŸã£ããŽãŒã«ããæåŸ
ãããæ¯ãèããç Žãå
¥åãæããŠããå Žåã¯ãç¹å®ã®å
¥åã§ã¢ãã«ãæåŸ
ãããæ¯ãèãã«éåããããšãè¿°ã¹ã bug_⊠ãšããå®çã蚌æããŸãããããããããšã§ãåäŸãã®ãã®ã Lean ã§æ€æ»ãããŸãã2 ã€ã®æ§è³ªã«ã€ããŠã¯ã蚌æã®ä»£ããã«æçæ€æ»ãæžããŸããïŒãããã®æ§è³ªã¯å€éšã®ãœãããŠã§ã¢ã«äŸåããŠãããLean ã§å¿ å®ã«ã¢ãã«åã§ããªãã£ãããã§ãïŒãæçæ€æ»ã察象ãšããã®ã¯ãäžéãŸã§ã®ãã¹ãŠã®å
¥åããŸãã¯åºå®ã®äžèЧã«ãããã¹ãŠã®ã±ãŒã¹ã ãã§ããã以å€ã¯å¯Ÿè±¡å€ã§ãã衚 1 ã§ 2 ä»¶ã®æçæ€æ»ãèšŒææžã¿ã«å«ãããå¥ã«æ°ããŠããã®ã¯ãã®ããã§ãã 5. åçŸããã åäŸãçºèŠãšããŠæ°ããã®ã¯ãæãå ããŠããªãå®éã®ã³ãŒããå®è¡ããã¹ã¯ãªããã§åãçµæãåºãå Žåã ãã§ãããã®ããã§ãå®éã®åŒã³åºãå
ããã®å
¥åã«å°éã§ãããã確ããããããèµ·ãããšãã«ãŠãŒã¶ãŒã«äœãèŠãããã調ã¹ãŸããã 倧åã®çºèŠã§ã¯ãããã«äžæ©é²ããŸãããä¿®æ£ã Lean ã§æžããã³ãŒããä¿ã€ã¹ãæ¯ãèããå€ããã«åé¡ãå¡ãããšã蚌æããã®ã§ããããã§èšŒæãããã®ã¯ä¿®æ£åŸã®ã¢ãã«ã®æ£ããã§ããä¿®æ£ãå®è£
ããã³ãŒãã®å€æŽã«ã€ããŠã¯ããã®å€æŽèªäœã®å·®åãã¹ããéããŸã§ã蚌æã¯äœãä¿èšŒããŸããã ã³ãŒãããŒã¹ 颿° æ§è³ª èšŒææžã¿ æçæ€æ» èŠã€ãã£ããšããžã±ãŒã¹ éšåçãªçµæãŸãã¯èŠ³å¯ Lean ã®å®ç ãã¹ãã±ãŒã¹ Kiro ããŒãã¹ïŒTypeScriptïŒ 15 51 36 0 9 6 111 23,281 Kiro CLIïŒRustãTypeScriptïŒ 8 29 23 0 6 0 86 65,000 Kiro CrewïŒPythonïŒ 3 16 11 2 3 0 38 9,657 åèš 26 96 70 2 18 6 235 97,938 衚 1: Kiro ããŒãã¹ãKiro CLIãKiro Crew ã®æ€èšŒçµæãšããããè£ä»ããæ€æ»ãåè¡ã®ãæ§è³ªã㯠4 ã€ã®çµæã®åã®åèšã§ãããèšŒææžã¿ãã¯ãå®çã«æžããä»®å®ãæºããã¢ãã«åãããã¹ãŠã®å
¥åã«ã€ããŠèšŒæããæ§è³ªã®æ°ã§ãããæçæ€æ»ãã¯ããµã€ãºã®äžéãŸã§ã®ãã¹ãŠã®ã±ãŒã¹ããŸãã¯åºå®ã®äžèЧã«ããã±ãŒã¹ã§æ€æ»ããæ§è³ªã®æ°ã§ãèšŒææžã¿ã«ã¯æ°ããŠããŸããããéšåçãªçµæãŸãã¯èгå¯ãã¯ãäžéšã ãã蚌æããæ§è³ªãšãå°éã§ããªãã³ãŒãã«ã€ããŠã®èгå¯ã®æ°ã§ãããLean ã®å®çãã«ã¯èšŒæã«å¿
èŠãªè£é¡ãå«ã¿ãŸããããã¹ãã±ãŒã¹ãã¯å·®åãã¹ãã§çæããå
¥åã®æ°ã§ãçŽç²é¢æ°ãªã 1 ã€ã®å
¥åãç¶æ
ãæã€é¢æ°ãªã 1 ã€ã®ã©ã³ãã ãªåŒã³åºãã®åã 1 ã±ãŒã¹ãšæ°ããŸãã Lean ã蚌æããããš Lean 㯠96 åã®æ§è³ªã®ãã¡ 70 åããããããå®çã«æžããä»®å®ãæºããã¢ãã«åãããã¹ãŠã®å
¥åã«ã€ããŠèšŒæããŸããïŒæ®ãã®æ§è³ªã¯ããã°ã®çºèŠããéšåçãªçµæãŸãã¯èгå¯ã«ãªããŸããïŒãããã§ã¯ããã®ãã¡ç¹ã«åœ¹ã«ç«ã€ãšèããŠãããã®ã玹ä»ããŸããã©ããå€ãã®å
¥åãã€ãã³ãã®é åºã«å·Šå³ããããã¹ãããã£ãšãæèã«ãªãéšåã ããã§ãã ã³ã³ããã¹ããšå±¥æŽ éè€ãããã¡ã€ã«ãåãé€ããŠãããªã¯ãšã¹ãã®ãã¬ãã£ãã¯ã¹ã¯ä¿ãããã åããã¡ã€ã«ãäœåºŠãæ·»ä»ããããšãKiro ããŒãã¹ã¯ãªã¯ãšã¹ããéãåã«ããã®å
容ã®ã³ããŒã 1 ã€ã ãæ®ããŸããäŒè©±ãé·ããªãã«ã€ããŠãã®åŠçã以åã®ã¡ãã»ãŒãžãå€ããŠããŸããšãã¿ãŒã³ããšã«ãã¬ãã£ãã¯ã¹ãå€ããããã£ãã·ã¥ãå¹ããªããªããããããããŸããç§ãã¡ã¯ãä»»æã®å±¥æŽ xs ãšä»»æã®æ°ããã¡ãã»ãŒãž ys ã«ã€ããŠã xs ã« ys ãç¶ãããã®ã®åŠççµæãã xs ã®åŠççµæã§å§ãŸãããšã蚌æããŸãããã€ãŸããã®åŠçã¯ããã¡ã€ã«ãããã€ãã£ãŠããã©ããªé åºã§ããåã®ã¿ãŒã³ã§ LLM ãèŠãå
å®¹ãæžãæããŸããããã®å®çã察象ãšããã®ã¯éè€ã®é€å»ã ãã§ããªã¯ãšã¹ãã®ãã¬ãã£ãã¯ã¹ã¯ããªã¯ãšã¹ããçµã¿ç«ãŠãã»ãã®åŠçã«ãå·Šå³ãããŸãã å±¥æŽã¯ç·šéãåèªã¿èŸŒã¿ãçµãŠãä¿ãããã Kiro ããŒãã¹ã¯ãåé€ããã¡ãã»ãŒãžãå
ã«æ»ããã¡ãã»ãŒãžãã»ãã·ã§ã³ãã¡ã€ã«ã«æ®ããå±¥æŽãçµã¿ç«ãŠããšãã«åé€ãåãæ¶ããåæ ããŸããç§ãã¡ã¯ããã®åæ ã 2 åè¡ã£ãŠã 1 åè¡ã£ãã®ãšåãçµæã«ãªãããšãçµæã¯ã¡ãã»ãŒãžãèœãšãã ãã§äžŠã¹æ¿ãã¯ããªãããšããã©ãŒã¯ããã»ãã·ã§ã³ã¯å¿
ããåé€ãåãæ¶ããåæ ããããšã®èŠªã®å±¥æŽããå§ãŸãããšã蚌æããŸãããåèªã¿èŸŒã¿ã®ããšã¯ããã¹ãŠã®ããŒã«ã«ãŒãïŒãã£ããç»é¢ã§ããŒã«åŒã³åºãã衚瀺ããæ¬ïŒãããŠãŒã¶ãŒãã©ã€ãã§èŠãŠããç¶æ
ã§çµãããŸãããã㯠8 ã€ããããŒã«åŒã³åºãã®ç¶æ
ïŒæ¿èªåŸ
ã¡ãå®è¡äžãæåãåãå
¥ãæžã¿ããšã©ãŒãåŠçæžã¿ã®ãšã©ãŒããã£ã³ã»ã«ãåŽäžïŒã®ãã¹ãŠã«ã€ããŠæãç«ã¡ãŸãã åãè©°ããåºåã¯äžéãè¶
ããªãã CLI ã®ãšãŒãžã§ã³ãã¯ãã·ã§ã«ã³ãã³ãã®åºåãªã©ã®ããŒã«ã®çµæããã³ã³ããã¹ããŠã£ã³ããŠã«å
¥ããåã«ãã€ãæ°ã®äžéãŸã§åãè©°ããŸããç§ãã¡ã¯ãæå¹ãª UTF-8 ã®ã©ããªæååã«ã€ããŠããåãè©°ããããã¹ãã UTF-8 ã®ãã€ãæ°ã§äžéãè¶
ããªãããšã蚌æããŸãããåãè©°ãã®éç¥ãæ«å°Ÿã«ä»ããå Žåãåãã§ïŒäžéããé·ãéç¥ã¯ãããèªäœãåãŸãããã«åãè©°ããããŸãïŒãéç¥ãä»ããªãå Žåã¯ãæåãéäžã§åå²ããã«åãŸããã£ãšãé·ãå
é éšåãæ®ãããšã蚌æããŸãããã¢ãã«ã¯ããã«ããã€ãã®ããã¹ãã®çŽ 4,000 ã±ãŒã¹ã§å®éã® Rust ã®é¢æ°ãšäžèŽããŸããã ã€ãã³ããã©ããªé åºã§å±ããŠããã»ãã·ã§ã³ã®ç¶æ
ã¯ä¿ãããã Kiro ããŒãã¹ã¯ãã»ãã·ã§ã³ãåŠçäžãããŠãŒã¶ãŒã®å
¥ååŸ
ã¡ããã¢ã€ãã«ããã¯ã©ã€ã¢ã³ãã«äŒããŸãããã®å€å®ã«ã¯ããã®ã»ãã·ã§ã³ãéå§ããããã¯ã°ã©ãŠã³ãã®ã¯ãŒã¯ãããŒãå«ãŸããŸããã¯ãŒã¯ãããŒã®ã€ãã³ãã¯å¥ã
ã®éåæåŠçã®äžã§æ±ãããã©ã®é åºã§çµãããã¯æ±ºãŸã£ãŠããªãããããã©ãã«ãŒã¯ã·ãŒã±ã³ã¹çªå·ã䜿ã£ãŠå
ã®é åºã«äžŠã¹çŽããŸããç§ãã¡ã¯ãå®è¡ãéå§ãäžæåæ¢ãçµäºããã€ãã³ãã«ã€ããŠãã©ã®é åºã§å±ããŠãå
ã®é åºã§å±ããå Žåãšåãç¶æ
ã«ãªãããšã蚌æããŸããããã®èšŒæã¯ãäžéšã®äžŠã¹æ¿ãã§ã¯ãªããã¹ãŠã®äžŠã¹æ¿ãã察象ãšããŸããã¢ãã«ãã6,000 åã®ã©ã³ãã ãªã€ãã³ãã®åïŒå€§åã¯é äžåã§å±ããã®ïŒã§å®éã®ãã©ãã«ãŒãšç
§ããåãããŸããã æš©é ãµããšãŒãžã§ã³ãã®å¶éã芪ããç·©ããªãããšã¯ãªãã Kiro ããŒãã¹ã¯ãµããšãŒãžã§ã³ããéå§ãããšãããµããšãŒãžã§ã³ãèªèº«ã®æš©éã®å€å®ã芪ã®å€å®ãšçµã¿åãããŸããç§ãã¡ã¯ããã®çµæãåžžã« 2 ã€ã®å€å®ã®ã©ã¡ããã§ãããåžžã«ãã®ãã¡å¶éã®å³ããã»ãã§ããããšããããŠãµããšãŒãžã§ã³ãããã®æåŠãæç€ºçãªç¢ºèªã®èŠæ±ã匱ããããããšã¯ãªãããšã蚌æããŸããããããã£ãŠãã®åŠçãéããŠã2 ã€ã®ããªã·ãŒãäœãå®ããŠããŠãã芪ãæåŠããããŸãã¯ç¢ºèªãæ±ããããŒã«åŒã³åºãããµããšãŒãžã§ã³ããæ¿èªããããšã¯ã§ããŸããããŸããããªã·ãŒãå³ããããŠãæåŠãæ¿èªã«å€ããããšã¯ãªãããšã蚌æããŸãããããã§ãå³ããããããšã¯ãèš±å¯ã確èªãæç€ºçãªç¢ºèªãæåŠãšããé åºã§ãå€å®ãå°ãªããšãåãã ãå¶éçã«ãªãããšãæããŸããããããŠãæ£èŠåãã絶察ãã¹ã .. ã䜿ã£ãŠã«ãŒãããäžã«åºãããªãããšã蚌æããŸããã 1 ã€ã®èš±å¯ãªã¹ãã 2 ã€ã®ããã¯ãšã³ãã§äœ¿ãã Crew ã§ã¯ããŠãŒã¶ãŒã CLI ã® allowedTools ã®åœ¢åŒã§ããŒã«ã®èš±å¯ãªã¹ããæžããšãCrew ãããã Kiro ããŒãã¹ã®ããªã·ãŒã®ãã¿ãŒã³ã«å€æããŸããç§ãã¡ã¯ 3 ã€ã®ç
§ååšïŒCrew ã®å€æãKiro ããŒãã¹ã®ããªã·ãŒã®ç
§ååšãCLI ã® glob ã®ç
§ååšïŒããã¹ãŠã¢ãã«åããããããã®ã¢ãã«ãå®éã®ã³ãŒããšç
§ããåãããããã§ãããã¯ã¹ã©ãã·ã¥ãå«ãŸãªãã©ã®ãšã³ããªã«ã€ããŠãã倿åŸã®ãã¿ãŒã³ã§å€å®ãã Kiro ããŒãã¹ããCLI ãã倧ããªæš©éãäžããªãããšã蚌æããŸããïŒ kas_le_cli ïŒãããã¯ã¹ã©ãã·ã¥ãå«ããšã³ããªã¯ãKiro ããŒãã¹ã§ CLI ãã倧ããªæš©éãäžããããšããããŸãããã㯠Crew ã® 3 ä»¶ã®çºèŠã®ãã¡ã® 1 ã€ã§ããããããšã³ããªãæåŠããä¿®æ£ã蚌æããŸããã CLI ãš Kiro Crew ã®ã¹ããŒããã·ã³ LLM ã®ãã©ãŒã«ããã¯ã¯å¿
ãæ¢ãŸãã LLM ããªã¯ãšã¹ããæåŠãããšãCLI ã®ãã©ãŒã«ããã¯ã®åŠçãå¥ã® LLM ã«åãæ¿ããŸããç§ãã¡ã¯ãæåŠãšåŒã³åºããã©ããªé åºã§èµ·ããŠãã1 ã€ã®ã¿ãŒã³ã§ 3 åãè¶
ããŠåãæ¿ããããšã¯ãªãããã®ã¿ãŒã³ã§ãã§ã«è©Šãã LLM ã«åãæ¿ããããšããªãããšã蚌æããŸããã 2 ã€ã®ãã£ã¹ãããã£ãŒãåãã¿ã¹ã¯ãåãããšã¯ãªãã è€æ°ã®ãã£ã¹ãããã£ãŒããã¥ãŒã§åŸ
ã£ãŠãã 1 ã€ã®ã¿ã¹ã¯ã奪ãåã£ãŠããæåãã claim åŒã³åºã㯠1 ã€ã ãã§ãããã®çŽåŸãã¿ã¹ã¯ã¯ admitted ã«ãªããã»ãã®ã©ã®ãã£ã¹ãããã£ãŒããã® claim åŒã³åºããæåŠãããŸãïŒåè¿°ã®äŸã®å®ç claim_exclusive ïŒãã¢ãã«ã¯ãã¹ãã¢ã®ããã¯ãããããŠãããšããã«ãã¹ãã¢ã®ååŒã³åºããäžå¯å㪠1 ã¹ããããšããŠæ±ããŸãããããã£ãŠãã®ä»®å®ã®ããšã§ã¯ãã©ããªé åºã§ããååŸå¯èœãªåãè¡ã«å¯Ÿã㊠2 ã€ã® claim åŒã³åºããæåããããšã¯ãããŸãããç«¶åããåŒã³åºãã代ããã«ããã¯ã®ãšã©ãŒã§å€±æããããšã¯ãããŸãããããã¯ãã®å®çã®ç¯å²å€ã§ãã ã¿ã¹ã¯ãã¥ãŒã¯å€ãã¯ãŒã«ãŒãç· ãåºãã Kiro Crew ã®ã¿ã¹ã¯ãã¥ãŒã§ã¯ãåã¿ã¹ã¯ã¯ 15 ã®ç¶æ
ããšãã queued ãã running ãåçš®ã®åŸ
ã¡ç¶æ
ãçµãŠã done ã failed ã cancelled ã®ããããã§çµãããŸãã claim åŒã³åºããæåãããã³ã«è¡ã®äžä»£ïŒgenerationïŒãå¢ããã¯ãŒã«ãŒããã®åŸã«è¡ãæžã蟌ã¿ã«ã¯ãèªåãæã€äžä»£ãä»ããŸããç§ãã¡ã¯ãã©ããªåŒã³åºãã®åã«ã€ããŠãäžä»£ãæžããªãããšã蚌æããŸããããã®ãããã¿ã¹ã¯ãæ°ããã¯ãŒã«ãŒã«åãããããšã¯ãå€ãã¯ãŒã«ãŒã®ãã§ã³ã¹ä»ãã®æžã蟌ã¿ã§è¡ãå€ããããšã¯ãããŸããã theorem stale_writer_fenced_out (lease : Nat) (ops : List Op) (r : Row) (o : Op) (g : Nat) (hg : g < r.gen) (ho : o.fencedBy = some g) : step lease o (run lease ops r) = run lease ops r ã¢ãã«ã¯ãSQLite ã§åãå®éã®ã¹ãã¢ãšãåèšçŽ 20,000 åã®åŒã³åºããããªã 4,500 åã®ã©ã³ãã ãªåã§äžèŽããŸããããããã®åã§ã¯åŒã³åºãã 1 ã€ãã€é ã«å®è¡ããã®ã§ã確ãããã®ã¯ååŒã³åºãã®ããžãã¯ã§ãã¹ãã¢ã®äžŠè¡åŠçã¯ç¢ºãããŠããŸããã䞊è¡ããã¯ãŒã«ãŒã«ã€ããŠã®äž»åŒµã¯ãåè¿°ã®äžå¯åæ§ã®ä»®å®ã«äŸæ ããŠããŸãã Lean ã®åäŸãšããŠèŠã€ãã£ããã° 18 ä»¶ã®ã³ãŒãã®æå³ã«ã€ããŠãã¢ãã«ã®äžã§åäŸãèŠã€ããããã®ãã¹ãŠãåæããã³ãŒãã§åçŸããŸããïŒã»ãã·ã§ã³éå§æã®ç«¶åã¯ã¢ãžã¥ãŒã«åäœã§åçŸïŒããã®èŠæš¡ã®ã³ãŒãã§ã¯ããããããšããžã±ãŒã¹ãããã®ã¯æ®éã®ããšã§ãã2026 幎 10 æ 1 æ¥ã« CLI ãš Kiro Crew ã® GitHub ã® issueããšãŒãžã§ã³ããµãŒããŒã®ãã«ãªã¯ãšã¹ããæ€çŽ¢ãããšãããã©ã®çºèŠã«ãäžèŽããæªè§£æ±ºïŒopenïŒã® issue ã¯ãããŸããã§ããããã ãããšãŒãžã§ã³ããµãŒããŒã®ããŒãžãããŠããªãïŒopenïŒãã«ãªã¯ãšã¹ãã®ãã¡ 1 ã€ã¯ 1 ä»¶ã®çºèŠãçŽããã®ã§ãå¥ã® 1 ã€ã¯ 1 ä»¶ã®çºèŠã®äžéšã説æããŠããŸãããã©ã®çºèŠããæ®éã§ãªãå
¥åãç¹å®ã®ã¿ã€ãã³ã°ãå¿
èŠãšããŸããããã€ãã¯å®å
šåŽã«åããŠå€±æããŸãããŠãŒã¶ãŒã«ããäžåºŠç¢ºèªãæ±ããããããLLM ã«èŠããããã¹ããæå³ããå°ãå€ããå°ãªããã§ãã倧åã«ã€ããŠã¯ãLean ã§ä¿®æ£ã蚌æããŸããã Kiro Crew ã®ã³ãŒãããŒã¹ã§èŠã€ãã£ã䞊è¡åŠçã®ãã°ããå
·äœçã«èŠãŠã¿ãŸãã ãã£ã³ã»ã«ããã®ã«å®è¡ããããžã§ãïŒ PR 25130 ãåç
§ïŒã Kiro Crew ã§ã¯ã決ããæå»ã«ãžã§ãã 1 åã ãå®è¡ã§ãããŠãŒã¶ãŒã¯å®è¡äžã®ãžã§ãããã£ã³ã»ã«ã§ããŸããã³ãŒãã®æå³ã¯ããã£ã³ã»ã«ããã1 åã ããã®ãžã§ãã¯äºåºŠãšå®è¡ãããªãããšãããã®ã§ãããã®æ¯ãèããç Žãæµãã¯æ¬¡ã®ãšããã§ãããžã§ããäœæ¥ã®éå§ãåŸ
ã£ãŠããããã ã«ãŠãŒã¶ãŒã Cancel run ãã¯ãªãã¯ãããšãCancel ã¯å®è¡ãæ¢ããŸããããžã§ããæå¹ãªãŸãŸæ®ããŸãããã®ããæ°ç§åŸã«ã¹ã±ãžã¥ãŒã©ãŒããžã§ããããäžåºŠå®è¡ããçµå±ãªãªãŒã¹ããŒããæçš¿ãããŠããŸããŸãããã£ã³ã»ã«ãããžã§ãã®äœæ¥ãå§ãŸãçŽåã®ããçãæéã«å
¥ãå¿
èŠãããããããã¹ãã§ã¯ãããèŠéããŸããLean ã¯ãããåäŸãšããŠèŠã€ããŸããããžã§ãã®ã©ã€ããµã€ã¯ã«ã®ã¢ãã«ã«ãããããã£ã³ã»ã«ã®ããšã«ãžã§ãã®äœæ¥ãå®è¡ãããŠçµããã10 åã®ã€ãã³ãã®åã§ããç§ãã¡ã¯ãã®åãå®éã®ã¹ã±ãžã¥ãŒã©ãŒã§åçŸããŸãããä¿®æ£ã¯ Cancel ã®åŠçã«æ¡ä»¶ã 1 ã€è¶³ãã ãã§ããä¿®æ£åŸã®ã¢ãã«ã«ã€ããŠã¯ãã©ããªã€ãã³ãã®åã§ããã£ã³ã»ã«ãããžã§ããåã³å®è¡ãããªãããšã Lean ã蚌æããŸãã /-- A counterexample. A user cancel that lands while the fire-time gate is awaited: `run_never_started` is set, so the finally does not auto-pause, and cancel() does not park a delete_after_run job. The next tick dispatches it again and its payload runs, after the user cancelled it. -/ def cancelInGate : List Ev := [tick, firstStep, enterExecute, cancelTake, cancelFinish, runFinally, tick, firstStep, enterExecute, gatePass] /-- Job status outcome. What a trace ends with: payloads started, dispatches, and whether the user cancelled. -/ def outcome (fixed : Bool) (dar : Bool) (es : List Ev) : Option (Nat à Nat à Bool) := (run fixed (init dar) es).map (fun t => (t.payloads, t.dispatches, t.userCancelled)) /-- Lean theorem that checks the counterexample. On the current code, for a job that deletes itself after it runs: the work ran once, the job was dispatched twice, and the user had cancelled it. -/ theorem bug_cancel_in_gate_runs_anyway : outcome false true cancelInGate = some (1, 2, true) := by decide ã»ãã«èŠã€ãã£ããã°ã¯ãäž»ã«æ¬¡ã®ã°ã«ãŒãã«åãããŸãã 䞊è¡åŠçã®ç«¶åã åæã«éå§ãã 2 ã€ã®ã»ãã·ã§ã³ãå¹²æžããããšããããŸãã session/new ã®åŠçäžã«å¥ã®ã»ãã·ã§ã³ã CLI ã«ç»é²ãããšãã»ãã·ã§ã³ã®éå§äžã«éãããæŽæ°ïŒããšãã°ã»ãã·ã§ã³éå§æã®ããã¯ããã®ããŒã«åŒã³åºãïŒã倱ãããããšããããŸãããã®çš®ã®ç«¶åã¯ãã¹ãã§èŠã€ãã«ãããã®ã§ãããã¹ããå®è¡ããã®ã¯ã€ãã³ãã® 1 ã€ã®é åºã ãã§ããã°ã¯å¥ã®é åºã§ããçŸããªãããã§ããLean ã§ã¯ãã»ãã·ã§ã³ã®æ°ãåãããã¢ãã«ã«ãããã»ãã·ã§ã³éå§ã®ã€ãã³ãã®ãã¹ãŠã®åã察象ã«å®çãæžããŸããã蚌æã¯éãããæŽæ°ã倱ãããã€ã³ã¿ãŒãªãŒãïŒ2 ã€ã®ã»ãã·ã§ã³ã®ã€ãã³ããå
¥ãæ··ããé åºïŒã bug_⊠ã®å®çãšããŠæžããLean ã§æ€æ»ããŸããããã®ããã§ããã®ã€ã³ã¿ãŒãªãŒãããã»ãã·ã§ã³ã®æŽæ°ãä¿çããŠåéãã CLI ã®å®éã®ã³ãŒãã§åçããŸããããã®ã³ãŒãã¯æãå ããã« import ããã¯ã©ã€ã¢ã³ãã®ãã³ãã©ãŒè¡šã®åãã«ã€ãªãã§ããŸããããã¯ã¢ãžã¥ãŒã«åäœã®åçŸã§ãåããŠãã CLI ã§ã®ãšã³ãããŒãšã³ãã®åçŸã§ã¯ãããŸããã 誀ã£ãåäœã§æž¬ã£ãäžéã Kiro ããŒãã¹ã® 9 ä»¶ã®çºèŠã®ãã¡ 7 ä»¶ã¯ãããã¹ããäžéã«åãŸãããã«åãè©°ãã颿°ã«ãããŸãã web_fetch ã«ã¯ãã€ãæ°ã®äžéããããŸãããããŒãžãåãè©°ãããšã㯠UTF-16 ã®ã³ãŒãåäœãæ°ãã JavaScript ã®æååã®é·ãã䜿ããäžéã®ãã€ãæ°ã®ååã®æ°ã®ã³ãŒãåäœãæ®ããŸããããã¯ãåã³ãŒãåäœã UTF-8 ã§ 2 ãã€ã以äžã§ããããšãåæã«ããŠããŸããäžåœèªãæ¥æ¬èªã®æå㯠1 ã³ãŒãåäœã§ãã UTF-8 ã§ã¯ 3 ãã€ããªã®ã§ãããããããŒãžã¯äžéã®æå€§ 1.5 åã®å€§ããã§è¿ã£ãŠããããšããããŸãããŸããæ¢å®ã®ã¢ãŒãã§ã¯ãããŒãžãåãè©°ããããšã瀺ãããŸãããUTF-16 ã®ã³ãŒãåäœã§æ°ããŠåãè©°ãããšãããã¹ãã®ãã¡ã°ãæåŸã«ããçµµæåãåå²ããŠããŸãããšããããŸãã grep_search ã¯äžèŽããè¡ã¯çãããŸãããååŸã®æèã®è¡ã¯çãããŸããããã®ãããããšãã° minify ããããã¡ã€ã«ã«ãããšãŠãé·ãæèã®è¡ã 1 è¡ããã ãã§ãäžèŽããè¡ãäžéå
ã®çµæããæŒãåºãããããšããããŸããã©ã®å Žåãäœãã倱æããããã§ã¯ãªããLLM ã«èŠããããã¹ããæå³ããå€å°å€ããå°ãªããã«ãªããŸãã ãšãŠã倧ããªã³ãã³ãã®åºåã ã·ã§ã«ã³ãã³ããããã¯ãã¯ãŒã¯ãããŒã®ã¹ãããã 2 29 â 24 åãè¶
ãã UTF-16 ã®ã³ãŒãåäœïŒASCII ã®ããã¹ãã§çŽ 512 MiBïŒãåºåãããšã詊ãããã«ãïŒmacOS arm64 äžã® Node 26.3.0 ãš V8 14.6ïŒã§ V8 ãäœããæé·ã®æååãè¶
ããŸããããŒãã¹ã¯ãV8 ã䜿ã Node ã®äžã§åããŸããKiro ããŒãã¹ã¯ãµã€ãºã®äžéããããåã«åºåã 1 ã€ã®æååã«ãŸãšããã®ã§ããšã©ãŒã¯äžéããå
ã«èµ·ããŸãããã®ãšã©ãŒãæãŸãããã®ã¯ãªããKiro ããŒãã¹ã®ææãããªããšã©ãŒã®ãã³ãã©ãŒãããã»ã¹ãçµäºãããããéããŠããã»ãã·ã§ã³ãçµãã£ãŠããŸããŸããKiro ããŒãã¹ã®ããã¯ã°ã©ãŠã³ãã®ã¿ãŒããã«çšã®åéåŠçã¯ãããšããšææ°ã®åºåã ããæ®ããŠããããã®åéåŠçã V8 ã®æååé·ã®å¶éã«æ±ºããŠéããªãããšã蚌æããŸããïŒ tail_join_safe ïŒãããã§ããã¹ãŠã®ã³ãã³ãã«ãã®åéåŠçã䜿ãããšãä¿®æ£ã«ãªããŸãã ã³ãŒã«ããªããŒãåŸã® spec ã®ã«ãŒã«ã Kiro ã® spec ã¢ãŒãã§ã¯ãã©ã€ãã®çµè·¯ãšåèªã¿èŸŒã¿ã®çµè·¯ã§ãæé»ã®ã«ãŒã«ãä»ããã¡ãã»ãŒãžãç°ãªããŸãããã®ãããã³ãŒã«ããªããŒãã®ããšã®ã¿ãŒã³ã¯ãã©ã€ãã®ã»ãã·ã§ã³ãéã£ãã¯ãã®ãªã¯ãšã¹ããšãããã«ç°ãªããåå©çšã§ãããã¬ãã£ãã¯ã¹ã 1 åå€ããŠããŸããŸãããã®çµæããã®ã¿ãŒã³ã§ã¯ãã£ãã·ã¥ãåå©çšã§ããªãããšããããŸãã æ¿èªãããã¹ã«å«ãŸãã glob ã®æåã CLI ã¯ãåžžã«èš±å¯ããããã¹ãããšã¹ã±ãŒãããã« glob ã®ãã¿ãŒã³ã«å€æããŸãã app/[slug]/page.tsx ã®ãã㪠Next.js ã®ã«ãŒãã§ã¯ãæ¿èªãããã¡ã€ã«ã«ã€ããŠããäžåºŠç¢ºèªãæ±ãããã app/s/page.tsx ã®ãããªå¥ã®ãã¹ãŸã§æ¿èªãããŠããŸããŸãïŒglob ã§ã¯ [slug] ã sãlãuãg ã®ãããã 1 æåã«äžèŽããããïŒãç§ãã¡ã¯ã¢ãã«ã§ä¿®æ£ã蚌æããŸãããå
ã«ãã¹ããšã¹ã±ãŒãããã°ãèš±å¯ã¯æ¿èªãããã¹ãšãã®é
äžã®ãã¡ã€ã«ã ãã«ãã£ã¡ãäžèŽããglob ã®æåãå«ãŸãªããã¹ã®æ±ãã¯å€ãããŸããã ã»ãã«ã 2 ã€ã®ã³ãŒãã®æå³ãæãç«ã¡ãŸããã§ãããããããç Žãå
¥åã«å°éããæ¬çªã®åŒã³åºãçµè·¯ã¯èŠã€ãããŸããã§ããããã®ããããããã¯çºèŠã§ã¯ãªã芳å¯ãšããŠæ°ããŠããŸãã衚 1 ã«ãã Kiro ããŒãã¹ã«ã€ããŠã® 2 ä»¶ã®èгå¯ãããã§ã18 ä»¶ã«ã¯å«ããŠããŸããã3 ã€ã®ã³ãŒãããŒã¹ã®ã©ãã§ããèŠã€ãã£ããã°ã®äžã«ãã»ãã¥ãªãã£äžã®åé¡ã«åœãããã®ã¯ãããŸããã§ããã åãã£ãã㚠蚌æã¯ããŒãã¹ã«ããåãã ã³ã³ããã¹ã管çãæš©éããããŠãã®åšãã®ã¹ããŒããã·ã³ã¯ãçãæ£ç¢ºãªå®çã«ãªããŸããæ¬¡ã®ã¿ãŒã³ã§ãåããã¬ãã£ãã¯ã¹ãåèªã¿èŸŒã¿ã®ããšã§ãåããªã¯ãšã¹ããã¡ããã© 1 ã€ã®ãã¡ã€ã«ã ãã«å¹ãæ¿èªãã€ãã³ããã©ã®é åºã§ãæãç«ã€çµæãªã©ã§ãããã®èåŸã«ãã颿°ã¯å°ããããã®ãŸãŸ Lean ã«çœ®ãæããããŸãã蚌æããæ§è³ªã®å€§åãšã18 ä»¶ã®çºèŠã®ãã¡ 15 ä»¶ã¯ãããã®é åã«ãããçºèŠã®å€§å㯠UTF-16 ãš UTF-8ããã¡ã€ã«ãã¹ãš glob ã®ãã㪠2 ã€ã®è¡šçŸã®å¢ç®ã«ãããŸããäž¡åŽã 1 ã€ã®èšèªã§æžãäžãããšã§ãã©ãã§é£ãéãããèŠããŸããã å·®åãã¹ãã¯èšŒæãšåããããéèŠã å·®åãã¹ãã¯ãLean ã®ã¢ãã«ã®èª€ããèŠã€ããŠçŽãã®ã«åœ¹ç«ã¡ãŸãããLean ã蚌æãå®äºã§ããªãã£ããšãã¯ãæ®ã£ããŽãŒã«ã倱æã®åå ãšãªãå
¥åã瀺ããŠããããšããããããŸããããã®ããã§ä¿®æ£ãæžãããã®ç¹å®ã®å
¥åã ãã§ãªããã¹ãŠã®å
¥åã§ãä¿®æ£åŸã®ã¢ãã«ãæå³ããæ¯ãèããæºããããšã蚌æããŸããã å¶çŽ èšŒæã瀺ãã®ã¯ãã¢ãã«ã®å®çŸ©ãšä»®å®ã®ããšã§ã® Lean ã¢ãã«ã®æ§è³ªã§ãããããå®éã®ã·ã¹ãã ã«ã€ããŠã©ããŸã§èªãããã¯ã蚌æã ãã§ã¯ç¢ºãããããªã次ã®ç¹ã«ããã£ãŠããŸãã ã¢ãã«ã¯ã³ãŒãã®åäœãšäžèŽããŠããªããã°ãªããªãã ãšãŒãžã§ã³ãã¯åã¢ãã«ããœãŒã¹ããæžããã®ã§ãã¢ãã«ãã³ãŒãã®åäœã®äžéšãåãããŒãããšã¯ããããŸããå·®åãã¹ãã¯ã¢ãã«ãå®éã®ã³ãŒããšç
§ããåãããŸãããã©ã³ãã ã«çæããå
¥åã§ãã確ãããªããããçæããªãã£ãå
¥åã§ã®éãã«ã¯æ°ã¥ããŸããããŸããã¿ã¹ã¯ãã¥ãŒãã¹ãã¢ã®ååŒã³åºããäžå¯å㪠1 ã¹ããããšããŠæ±ãããšã®ããã«ãæç€ºããä»®å®ã«äŸæ ããŠããã¢ãã«ããããŸãã å®çã¯ã³ãŒãããã¹ãããšãè¿°ã¹ãŠããªããã°ãªããªãã ãšãŒãžã§ã³ãã¯åå®çãããã¥ã¡ã³ãã³ã¡ã³ããèšèšäžã®äžå€æ¡ä»¶ãåŒã³åºãç®æããæžããç§ãã¡ããããã¬ãã¥ãŒããŸãããå®çãæå³ããæ¯ãèãã®äžéšãæžãæŒãããŠããã°ã蚌æãæåããŠããã°ãèŠéãããšããããŸãã ã¢ãã«ã®åã¯å¿ å®ã§ãªããã°ãªããªãã ã¢ãã«ã Lean ã®äžéã®ãªãèªç¶æ°ã䜿ã£ãããããŒã¿æ§é ãæœè±¡åãããããŠããç®æã§ã¯ããªãŒããŒãããŒãæµ®åå°æ°ç¹ã®æ¯ãèããæäœã®ã³ã¹ãã¯æããããŸãããUTF-8 ã UTF-16 ã®é·ãã®ããã«ãã³ãŒãã®æ¯ãèãã«ã€ããŠã®å³å¯ãªåœé¡ïŒå®çãè£é¡ïŒãå€ã®è¡šçŸã«äŸåããç®æã§ã¯ã衚çŸãæ£ç¢ºã«ã¢ãã«åããŸããã ä¿¡é Œããåºç€ã¯ã«ãŒãã«ããåºãã 蚌æã¯ Lean ã®ã«ãŒãã«ã«äŸåããŸããå·®åãã¹ãã¯ããã«ãLean ã®ã³ã³ãã€ã©ãŒãäž¡åŽã«åãå
¥åãäžãããã¹ãããŒãã¹ãå®éã®ã³ãŒãã®ã©ã³ã¿ã€ã ã«ãäŸåããŸãã native_decide ïŒåœé¡ãã³ã³ãã€ã«ããŠå®è¡ããçåœãå€å®ãã Lean ã®æ©èœïŒã䜿ã 17 åã®å®çã¯ãLean ã®ã³ã³ãã€ã©ãŒãšãããããã«ãã«äœ¿ã C ã®ããŒã«ãã§ãŒã³ãä¿¡é ŒããŠããŸãããã ãããã® 17 åã¯ã©ãããèšŒææžã¿ãšããŠæ°ããæ§è³ªã®æ ¹æ ã«ã¯äœ¿ã£ãŠããŸããããããã¯æçæ€æ»ãåäŸã1 ã€ã®å¯Ÿç
§ã±ãŒã¹ã§ãåäŸã¯ãã¹ãŠå®éã®ã³ãŒãã§ãåçŸããŠããŸãã çµæã¯ã³ãããã«çµã³ä»ããŠããã åã¢ãã«ãèšè¿°ããã®ã¯ãåæããã³ãããã®æç¹ã®ã³ãŒãã§ãããã®åŸã®ã³ãŒãã®å€æŽã¯ãã¢ãã«ãæŽæ°ããŠå·®åãã¹ããåã³éããŸã§å¯Ÿè±¡å€ã§ãã ãããã®åé¡ã¯ãèªå圢åŒåïŒautoformalizationïŒã®åéã§ã¯ããç¥ãããŠããŸããèªå圢åŒåã§ãã¡ã°ãé£ããã®ã¯ãèªç¶èšèªã§æžãããæ°åŠã®äž»åŒµã§ãããå¥ã®ããã°ã©ãã³ã°èšèªã®ã³ãŒãã§ãããLean ã®åœé¡ãå
ã®ãã®ãå¿ å®ã«æããŠãããšç¢ºãããããšã§ããçºèŠã«ã€ããŠã¯ãå®éã®ã³ãŒããæ±ºçãä»ããŸããååäŸãå®éã®ã³ãŒãã§åçããŠãããããã§å€±æããã°ãã¢ãã«ãšã¯ç¬ç«ã«ãã°ã確å®ããŸãã蚌æãä¿¡é Œããæ ¹æ ãšããŠã¯ãå·®åãã¹ããšå®çã®èšè¿°ã®ã¬ãã¥ãŒã§ååã ãšå€æããŸããããã®ææ³ãåœãŠãã®ã¯ãåœé¡ãå°ããç°¡æœã«æžãããã®å€§åã 2 ã€ã®è¡šçŸã®å¢ç®ã«ããã广ãåºããã 26 åã®é¢æ°ã§ããåçºèŠãããããåŒã³åºãã³ãŒãããå°éã§ãããã©ããã倿ããŸããã ã³ã³ããã¹ã管çã®ä»äºã«ãšã£ãŠã®æå³ Kiro ã®ã³ã³ããã¹ã管çã¯ãã³ã³ããã¹ããŠã£ã³ããŠã®å
容ã«ã¯äžéããããåèªã¿èŸŒã¿ããã»ãã·ã§ã³ã¯å€ãããªããããã³ãããã£ãã·ã¥ã¯äžé£ã®åŠçãéããŠä¿ãããããšãã£ãããŒãã¹ã®æ§è³ªã®äžã«æãç«ã£ãŠããŸãããããŸã§ãããããåæã¯èšèšããã¥ã¡ã³ããšåäœãã¹ãã®äžã«ãããããŸããã§ãããæ¬èšäºã§åãäžãã颿°ã«ã€ããŠã¯ããããã Lean ã¢ãã«ã«ã€ããŠã®å®çã«ãªãããããããã©ã³ãã ã«çæããå
¥åã§ã®å·®åãã¹ãã«ãã£ãŠå®éã®ã³ãŒãã«çµã³ä»ããŠããŸãã察象ã¯åæããã³ãããæç¹ã®ãããã®é¢æ°ã§ãããŒãã¹å
šäœã§ã¯ãããŸããã ãããä»åŸã®ããŒããããã®åå°ã«ãªããŸããæ©èœãèšèšããæ®µéã§æ§è³ªã 1 ã€ãã€å®çãšããŠæžããã³ãŒããå€ãããã³ã«å·®åãã¹ããæµãçŽããŠãã¬ãã¥ãŒã®åã«ãªã°ã¬ãã·ã§ã³ãèŠã€ããããããèšç»ã§ããæé ã¯èªååãããŠããŸãããå®çã®èšè¿°ãšçºèŠã¯ãããã人ãã¬ãã¥ãŒããå¿
èŠããããŸãããã®ãããKiro ã®ã»ãã®ãªããžããªã«æ€æ»ãåºãããããã©ããã¯ãèšç®è³æºã ãã§ãªãã¬ãã¥ãŒã«ãããããåŽåã«ãå·Šå³ãããŸããç®æããŠããã®ã¯ãããŒãã¹ã®äžæ žã®æ¯ãèãã®ãã¡ãåæãšããŠçœ®ãã®ã§ã¯ãªã蚌æããããã®ãå¢ãããŠããããšã§ãã èªåã®ã³ãŒãã§è©Šã Lean ãå§ããã«ã¯ã Lean ã®ããã¥ã¡ã³ã ãåç
§ããŠãã ãããKiro ã®ãšãŒãžã§ã³ãããŒãã¹ã®ä»çµã¿ã«ã€ããŠã¯ã One agent, every surface ãã§è©³ãã説æããŠããŸãã Kiro ãããŠã³ããŒã ããŠããèªèº«ã®ã³ãŒãããŒã¹ã§è©ŠããŠã¿ãŠãã ããã åæã®èè
Yaroslav KharkovãFerhat Erataã Behrooz Omidvar-Tehrani ã Rajdeep Mukherjee ïŒãããã Applied ScienceïŒ ç¿»èš³è
ã«ã€ããŠ çš²ç° å€§éž â ããªãã AWS Japan ã§åã Kiro ããããªãæããœãªã¥ãŒã·ã§ã³ã¢ãŒããã¯ããæ®æ®µã¯è£œé æ¥ã®ã客æ§ãæ¯æŽããŠããŸãããã®æŽ»åã®åããæè¿ã¯ AI é§åéçºã©ã€ããµã€ã¯ã« (AI-DLC) ã®æ¥æ¬ã®ã客æ§ãžã®åžææŽ»åããã€ã€ã Kiro ã®ããã° ãªã©ãå·çããŠããŸãã