오늘 Hacker News에서 LLM을 활용한 seL4 커널 정형 검증에 관한 논문을 보게 되었다. seL4라는 이름을 보는 순간, 십여 년 전 임베디드 시스템을 다루던 시절이 떠올랐다.
그때는 정형 검증이라는 것이 학계의 전유물처럼 느껴졌다. 수학적으로 코드의 정확성을 증명한다니, 얼마나 아름다운 개념인가. 하지만 현실의 프로젝트에서는 테스트 코드 하나 더 짜는 것도 빠듯했던 기억이 난다.
정형 검증, 왜 어려웠나
정형 검증의 핵심은 “이 코드가 스펙대로 동작함을 수학적으로 증명한다”는 것이다. 버그가 있을 수 없음을 보장하는 것. 하지만 그 증명을 작성하는 것 자체가 원래 코드보다 몇 배는 더 복잡했다.
seL4 마이크로커널이 완전한 정형 검증을 달성했을 때, 업계에서는 경이로운 성과라고 했다. 10년 이상의 노력과 수십만 줄의 증명 코드가 들어갔다고 들었다.
LLM이 바꾸는 게임
이번 논문을 보면서 생각했다. LLM이 정형 검증의 문턱을 낮출 수 있을까? 논문에서는 LLM을 활용해 Isabelle/HOL 증명을 자동 생성하는 방식을 다룬다. 완벽하지는 않겠지만, 방향성이 흥미롭다.
40대가 되어 보니, 기술의 민주화라는 것이 어떤 의미인지 체감하게 된다. 예전에는 소수의 전문가만 접근할 수 있던 것들이 점점 많은 사람에게 열리고 있다. 정형 검증도 그런 길을 갈 수 있을까.
현실적인 의미
안전이 중요한 시스템들—의료기기, 자율주행, 항공우주—에서 정형 검증은 여전히 꿈같은 이야기다. 비용이 너무 높기 때문이다. 만약 LLM이 그 비용을 획기적으로 낮춘다면, 우리가 사용하는 소프트웨어의 신뢰성이 근본적으로 달라질 수 있다.
아직은 연구 단계지만, 5년 후, 10년 후가 기대된다. 내가 은퇴할 때쯤이면 “버그 없는 코드”가 당연한 시대가 올지도 모르겠다.
이 포스팅은 쿠팡 파트너스 활동의 일환으로, 이에 따른 일정액의 수수료를 제공받습니다.
