글로벌 금융 기업 제인 스트리트(Jane Street)가 소프트웨어의 정확성을 수학적으로 증명하는 '형식 기법(Formal Methods)'에 대한 오랜 회의적인 입장을 바꾸고 전담 팀을 신설했습니다. 과거에는 극히 일부 특수 사례를 제외하고는 비용 대비 효용이 낮다고 판단했지만, 최근 AI 에이전트 코딩의 확산이 이러한 인식을 근본적으로 변화시켰습니다.
형식 기법은 소프트웨어가 의도한 대로 동작하는지 엄격하게 검증하는 도구입니다. 예를 들어, 보안이 중요한 seL4 마이크로커널의 경우 8,700줄의 C 코드를 검증하는 데 25인년(人年)이 소요될 정도로 막대한 자원과 시간이 필요했습니다. 코드 한 줄당 약 23줄의 증명과 반 인일(人日)의 검증 작업이 필요했죠. 하지만 AI 에이전트가 코드를 생성하기 시작하면서 상황이 달라졌습니다. 에이전트가 만든 코드는 빠르게 늘어나지만, 실제 출시 가능한 품질과는 차이가 있으며 복잡하고 예측 불가능한 버그를 포함하는 경우가 많습니다. 제인 스트리트는 이러한 '검증 병목'을 해소하고 에이전트에 더 강력한 피드백을 제공하기 위한 핵심 수단으로 형식 기법의 가치를 재평가하고 있습니다.
제인 스트리트가 이 분야에 뛰어드는 이유는 크게 두 가지입니다. 첫째, 자체적으로 사용하는 프로그래밍 언어인 OxCaml을 깊이 통제할 수 있어 증명 지향 기법에 맞게 언어를 조정하고 통합할 수 있다는 점입니다. 둘째, 이미 정교한 타입 시스템(Type System)에 익숙하고 고품질 소프트웨어 개발에 대한 관심이 높은 개발자 커뮤니티를 보유하고 있어, 새로운 형식 기법을 빠르게 도입하고 발전시킬 수 있는 환경이 조성되어 있습니다. 이는 AI가 생성하는 코드의 신뢰성과 안정성을 확보하는 데 있어 형식 기법이 필수적인 역할을 할 것이라는 업계의 기대를 반영하며, 프로그래밍 패러다임의 변화를 예고합니다.