Um desenvolvedor usou Claude Opus 5.5 para formalizar o CPython em Lean, em 613.318 linhas

O desenvolvedor broyojo42 diz que usou Claude Opus 5.5 para escrever uma formalização do CPython em Lean: 613.318 linhas que reproduzem os detalhes internos do Python linha por linha, testadas com o interpretador real e verificadas pelo Lean. Segundo ele, durante o processo, o modelo encontrou bugs reais no Python, incluindo falhas causadas por código Python comum.

A publicação é o relato do próprio autor; ela tinha 2.066 pontos no X em 10 de novembro. Charlie Marsh, da Astral, compartilhou a publicação.