오픈소스중요도: 보통오픈소스 AI 코딩 에이전트 'Forall', 증명 가능한 코드 생성Hacker News2026년 7월 16일 · 8시간 전Forall은 코드를 작성할 때 그 코드가 올바르다는 것을 기계가 검증할 수 있는 증명까지 함께 만들어주는 오픈소스 AI 코딩 에이전트다. 일반 AI 코딩 도구는 코드만 내놓고 그게 맞는지는 사람이 테스트해봐야 알 수 있지만, Forall은 Lean이나 Dafny 같은 정형 검증 도구를 이용해 코드가 명세한 대로 동작한다는 걸 수학적으로 증명한 결과물을 함께 제공한다.현재는 3개 프로그래밍 언어만 이런 방식의 검증을 지원하는 초기 단계다. 제작팀은 정형 검증이나 AI 코딩 에이전트에 관심 있는 사람들의 피드백을 구하고 있다.핵심 포인트오픈소스 AI 코딩 에이전트로, 코드와 함께 기계가 검증 가능한 증명을 생성함Lean, Dafny 같은 정형 검증 도구 활용 대상 커뮤니티를 겨냥현재 3개 프로그래밍 언어만 증명 검증을 지원하는 초기 단계제작팀이 정형 검증·AI 코딩 에이전트 관심자들의 피드백을 구하는 중원문 보기 ↗↗ 공유