Bend, 증명으로 AI 코딩 실수를 막고 GPU까지 쓰는 언어

Bend는 AI가 작성한 코드에서 발생할 수 있는 실수를 수학적 증명으로 걸러내는 것을 목표로 하는 새 프로그래밍 언어다. C에 가까운 실행 속도, CUDA 기반 병렬성, Lean 계열의 증명 시스템을 한데 묶어 AI 에이전트가 만든 코드를 사람이 전부 읽지 않아도 검증할 수 있게 하려는 시도다. 자연어 프롬프트의 모호함을 줄이고, 구현이 의도한 규칙을 지켰는지 기계적으로 확인하는 데 초점을 둔다.

Bend는 네이티브 코드로 컴파일된다. 단일 코어에서는 C에 거의 맞먹는 성능을 내고, 같은 바이너리가 16개 코어나 GPU에서도 실행되며 최대 100배까지 빨라진다고 설명한다. 개발자가 스레드, 락, GPU 커널을 직접 다루지 않아도 작업을 둘로 나누면 런타임이 가용한 코어에 호출을 분산했다가 다시 합친다. pow2 예제는 4,096개의 GPU 코어에서 돌아간다.

핵심 기능은 LAWS.bend다. 절대 깨지면 안 되는 규칙을 법으로 선언해 두면, AI가 그 법을 위반하는 변경을 커밋하지 못하도록 막는다. 게임 예시에서는 보드가 감싸지도록(wrap around) 수정해 달라는 요청에 대해, 승리로 이어지는 수순이 없어야 한다는 법을 어기는 패치는 병합되지 않는다. AI는 벽을 만들고 법이 유지된다는 증명을 완성할 때까지 재시도해야 하며, 결과적으로 버그가 병합되는 일이 수학적으로 불가능해진다는 주장이다.

Bend의 타입 검사기는 Lean이나 Rocq처럼 증명 검사기 역할을 한다. 다만 중간 규모 코드베이스에서 분 단위가 걸릴 수 있는 기존 도구와 달리, Bend는 최대 1초 안에 검사를 끝낸다고 한다. 그래서 AI 에이전트가 변경할 때마다 곧바로 검증할 수 있다. LAWS.bend는 증명으로 뒷받침되는 AGENTS.md에 비유되며, 실수하지 말라는 지시를 타입 검사 수준으로 끌어올리는 셈이다.

사용 흐름도 단순하다. 설치 스크립트를 실행한 뒤 에이전트에게 Bend를 쓰라고 지시하고, LAWS.bend에 중요한 규칙을 모아 두며, 커밋 전에 bend PROOF.bend를 돌리게 하는 방식이다. 가능한 코드는 모두 병렬화하도록 요청하라고 권한다. 절대 깨지면 안 되는 대상에 대해 법을 작성하게 하고, 빠르게 돌리고 싶은 부분은 병렬화하게 하라는 조언도 함께 제시한다.

배경에는 AI 코딩 에이전트의 확산과, 머지않아 인간이 코드를 직접 쓰고 읽지 않을 수 있다는 전제가 있다. 사람이 모든 코드를 읽지 않고도 AI가 만든 소프트웨어를 받아들이는 상황이 늘면서, 자연어 요구사항만으로는 정확성을 보장하기 어려워졌다. 테스트와 정적 타입, 형식 검증은 각각 강점이 있지만 AI가 매 변경마다 빠르게 확인하기에는 부담이 있다. Bend는 의도를 법으로 표현하고 증명으로 검사하는 방식을 통해 이 간극을 노린다.

한국 개발자에게 의미가 있는 부분은 커밋 전 검증 자동화다. AI 에이전트가 만든 변경을 그대로 병합하는 대신, 규칙 위반을 증명 검사로 차단하는 파이프라인을 실험해 볼 수 있다. 병렬화가 필요한 연산을 CPU와 GPU로 확장할 때 스레드와 커널을 직접 작성하지 않아도 된다는 점도 백엔드 워크로드에서 매력적이다. 다만 기존 언어 생태계, 라이브러리, 디버깅 도구와의 통합 수준은 별도로 확인해야 한다.

Bend는 아직 젊은 프로젝트다. 버그가 있을 수 있으니 문제가 생기면 이슈를 열어 달라고 요청하며, Linux와 macOS의 백엔드 환경에서 가장 잘 동작한다고 안내한다. 전체 언어 안내는 GUIDE.md에 있고 bend guide 명령으로 볼 수 있다. 이론적 토대는 affine dependent type theory를 다룬 BendTT 논문, CPU와 GPU를 위한 병렬 런타임은 BendRT 논문으로 정리되어 있다. 도입 전에는 증명 검사 범위와 성능 수치가 자신의 워크로드에서도 재현되는지 직접 검증하는 편이 좋다.