로빈후드 CEO, 2년 안에 모든 코드 형식 검증 전망

테네프는 4일(현지시간) X에 “모든 코드가 2년 안에 형식 검증을 거칠 것”이라고 썼다. 그는 안전상 중요한 코드부터 시작해 적용 범위를 넓힐 것이라고 덧붙였다.

관련 글은 공개 게시물 색인에 수록돼 있다. 테네프는 적용 순서를 제시했지만 특정 기업의 도입 일정은 밝히지 않았다.

로빈후드의 공식 경영진 소개는 테네프를 로빈후드 CEO이자 Harmonic의 공동 창업자·집행 회장으로 소개한다. 형식 검증 도구를 만드는 회사와 그의 관계는 이번 전망의 맥락이다.

Harmonic은 10월 27일 발표문에서 형식 검증 도구 Aristotle의 지원 범위를 소프트웨어와 하드웨어로 넓혀 C와 Verilog를 지원한다고 밝혔다. 회사는 Aristotle을 현재 이용할 수 있다고 발표했다. Harmonic 공식 발표

형식 검증은 프로그램에 미리 지정한 속성이 정해진 시스템 범위 안에서 모든 가능한 입력에 대해 성립하는지 수학적으로 증명하는 절차다. 테스트가 일부 실행 사례를 확인하는 것과 달리, 형식 검증은 명세로 정한 범위의 속성을 증명한다.

Harmonic은 Aristotle이 코드에서 검증할 속성을 제안하고, 개발자가 이를 검토해 저장소에 반영하는 작업 흐름을 설명했다. 개발자는 코드가 바뀔 때마다 검증을 실행할 수 있다.

C 검증은 지정된 요구 조건에 따른 기능의 정확성과 일부 정의되지 않은 동작의 부재를 다룬다. Aristotle 소프트웨어 검증 문서는 기본 결과물로 메모리 안전성 증명을 제시한다.

메모리 안전성 증명은 함수 호출자가 정해진 사전 조건을 충족할 때 경계를 벗어난 읽기·쓰기, 널 포인터나 해제된 포인터의 역참조, 초기화되지 않은 값 읽기, 부호 있는 정수 오버플로 같은 문제를 확인한다. 이는 명시된 조건을 지키는 실행 범위에서의 결과다.

검증 문서는 함수별로 증명한 내용과 호출자가 지켜야 할 조건을 결과에 표시한다. 외부 라이브러리처럼 검증하지 않고 동작을 가정한 부분도 따로 밝힌다.

Verilog 설계에서는 제어 경로의 안전성과 동작이 계속 이어지는지를 확인하고, 데이터 경로의 수학적 속성도 검증한다. 이 역시 Aristotle이 지원한다고 발표한 형식 검증 범위에 해당한다.

증명 결과는 개발자의 목적 자체가 아니라 문서화된 속성에 대한 답이다. 요구 조건이 실제 의도를 제대로 담지 못했다면 그 조건을 증명해도 프로그램이 의도대로 동작한다는 의미는 아니다.

Harmonic은 AI 시스템이 생성하는 코드가 늘어나는 가운데 코드 검토가 중요한 실패 지점이 됐다고 설명했다. 회사는 형식 검증을 통해 지정한 속성을 더 넓은 입력 범위에서 확인하는 방법을 제시했다.

코드 작성 속도가 빨라져도 제품 출시까지의 과정이 함께 빨라지는 것은 아니라는 사례도 있다. 본지는 오라클이 생성형 AI로 코드 작성 기간을 줄였지만 테스트·검증·배포 절차가 남은 사례를 보도한 바 있다.

미국 샌디아국립연구소가 공개한 형식 검증 워크숍 보고서는 형식 검증 도구의 사용성과 결과 해석을 널리 적용하기 위한 과제로 꼽았다. 보고서는 도구가 전문 인력에게만 쓰이는 어려운 도구로 남을 수 있다고 지적했다.

보고서에는 도구의 처리 범위에 맞춰 검증 대상을 제한한 사례도 담겼다. 대규모 증명은 기존 도구의 한계를 넘어 작업량을 늘릴 수 있어 확장성도 과제로 제시됐다.