Leanstral: 신뢰할 수 있는 바이브 코딩을 위한 오픈소스 기반 | Mistral AI

미스트랄 AI가 Lean 4용 오픈소스 AI 에이전트 ‘Leanstral’을 출시해 형식적 증명을 생성하고 검증할 수 있게 했다.

모델은 Apache 2.0 라이선스로 공개됐고, 무료 API와 MCP 도구 지원도 제공된다.

미스트랄은 Leanstral이 단순한 데모가 아니라 실제 형식 검증 저장소와 증명 엔지니어링에 맞춰 최적화됐다고 설명했다.

새 벤치마크 FLTEval로 폐쇄형·오픈소스 코딩 시스템과 성능을 비교 평가했다.