Bend 2 공개, AI 코드 규칙 위반 시 컴파일 실패하는 형식 증명 언어

AI 코드의 신뢰성 확보를 위한 '법칙 주도 개발'

Bend 2는 AI 코딩 에이전트가 작성한 코드가 사람이 명시한 규칙(LAWS.bend)을 위반할 경우 컴파일 단계에서 실패하도록 강제하는 새로운 프로그래밍 언어다. 2026년 9월 공개되었으며, Apache 2.0 라이선스를 채택했다. 핵심은 자연어 프롬프트나 테스트가 아닌, 컴파일러가 검증 가능한 형식 증명(PROOF.bend)을 통해 코드의 정확성을 보장하는 '법칙 주도 개발(Law-Driven Development)' 패러다임이다.

기술적 특징 및 성능

• 언어 구조: Python 문법과 Lean/Haskell 의미론, Rust 자원 관리 방식을 결합했다. 아핀(Affine) 타입 시스템을 기본으로 하여 변수의 재사용을 엄격히 통제하며, 이를 통해 메모리 안전성과 종료성을 보장한다.
• 성능: C 수준 속도를 목표로 하며, GPU 실행을 지원한다. Apple M4 Max 기준 CPU 16코어에서 단일 코어 대비 7.6~12.1배 가속을 달성했으며, 균일한 연산에서는 GPU가 CPU보다 크게 앞서지만 분기가 많거나 작업량이 치우친 경우 CPU보다 느릴 수 있다. 또한 GPU 성능은 Apple 칩의 등급(M4 Max vs 기본 M4)에 따라 크게 좌우된다.
• 증명 속도: 정의 12,800개 기준 증명 검사 시간이 0.29초로, Lean(36.2초)이나 Rocq(5.99초)보다 훨씬 빨라 AI 에이전트의 반복적인 코드 생성 및 검증 루프에 적합하다.

한계 및 주의사항

• 생태계 초기 단계: Windows 미지원, TLS/HTTP/JSON/정규표현식 라이브러리 부재, 에디터 및 디버거 미제공 등 생태계가 매우 초기 상태다.
• 컴파일러 신뢰성: 컴파일러 코드의 99%가 AI로 작성되어 아직 완전히 감사되지 않았으며, 형식화 모델과 실제 구현 간 불일치로 인한 무모순성 버그 가능성이 존재한다.
• 규칙의 한계: 법칙 자체의 논리적 오류는 검증할 수 없으므로, 빈 리스트 통과 등 엣지 케이스를 막기 위해 보조 법칙을 병행해야 한다.