최근 Astrio(아스트리오)가 개발한 오픈소스 AI 코딩 에이전트 'Forall(포올)'이 소프트웨어 개발 방식에 새로운 가능성을 제시하고 있습니다. Forall은 단순히 코드를 생성하는 것을 넘어, 생성된 코드가 사양(specification)에 따라 정확하게 작동함을 수학적으로 증명하는 '기계 검증 가능 증명(machine-checkable proofs)'을 함께 제공합니다. 이는 소프트웨어의 신뢰성과 안정성을 획기적으로 높일 수 있는 잠재력을 가지고 있습니다.
Forall은 현재 타입스크립트(TypeScript), 자바(Java), 러스트(Rust) 세 가지 프로그래밍 언어를 지원하며, 사용자 수요에 따라 지원 언어를 확대할 예정입니다. 이 에이전트는 로컬 저작(local authoring) 및 호스팅된 검증(hosted verification) 어댑터를 포함하는 Rust 크레이트(crate) 형태로 제공되며, 개발자들은 이를 통해 코드를 작성하고 그 정확성을 검증할 수 있습니다. 특히, 형식 검증(formal verification) 분야에 관심 있는 개발자들에게 유용한 도구가 될 것으로 보입니다.
이러한 접근 방식은 소프트웨어 버그를 줄이고 개발 프로세스의 효율성을 높이는 데 크게 기여할 수 있습니다. 전통적인 테스트 방식으로는 발견하기 어려운 복잡한 오류를 수학적 증명을 통해 사전에 방지할 수 있기 때문입니다. Forall과 같은 AI 에이전트의 등장은 고신뢰 시스템, 보안이 중요한 애플리케이션 등 정확성이 필수적인 분야에서 소프트웨어 개발의 패러다임을 변화시킬 중요한 전환점이 될 것입니다. 개발자들은 이제 AI의 도움을 받아 더욱 견고하고 신뢰할 수 있는 소프트웨어를 구축하는 데 집중할 수 있게 될 것입니다.