벤드(Bend)가 AI가 작성한 코드의 오류를 증명 검사를 통해 차단하는 프로그래밍 언어를 제시했다. 벤드 공식 사이트(bend-lang.com)는 9월 18일 벤드가 C에 가까운 단일 코어 실행 속도와 CUDA 기반 GPU 병렬 처리를 함께 제공한다고 설명했다.
벤드의 실행 속도와 증명 검사
벤드는 코드를 네이티브 코드로 컴파일하며, 한 코어에서 실행할 때 C와 거의 같은 속도를 낸다. 같은 바이너리는 16개 코어 또는 GPU에서도 실행할 수 있고, GPU를 사용하면 단일 코어 실행보다 최대 100배 빠르게 동작할 수 있다는 것이다. 벤드는 작업을 여러 부분으로 나누면 사용 가능한 코어 전체에 호출을 분산한 뒤 결과를 다시 합친다.
기존 병렬 프로그래밍처럼 스레드나 잠금 장치를 직접 다루거나 GPU 커널을 작성할 필요도 없다고 설명했다. 예시로는 `pow2` 연산을 4096개 GPU 코어에서 실행하는 장면을 제시했다. 벤드의 타입 검사기는 린(Lean)과 로크(Rocq)처럼 증명 검사기로 작동하지만, 중간 규모 코인베이스(codebase)를 검사하는 데 최대 1초가 걸린다. 린과 로크의 검사는 중간 규모 코인베이스에서 수분이 걸릴 수 있어, 벤드는 AI 에이전트가 코드가 바뀔 때마다 검사할 수 있다는 점을 내세웠다.
LAWS.bend로 AI 코드 검증
벤드는 자연어 명령만으로는 AI가 사용자의 의도를 정확히 구현했는지 확인하기 어렵다는 문제에 증명을 적용했다. `LAWS.bend` 파일에 절대 깨져서는 안 되는 규칙을 선언하면, 이후 AI가 해당 규칙을 위반하는 코드를 제출하지 못하도록 검사한다. 예시에서는 게임 규칙을 ‘승리가 불가능해야 한다’고 정한 뒤, 클로드(Claude)에게 게임판이 이어지도록 수정하라고 지시했다.
규칙 파일이 없을 때는 버그가 실제로 작동했지만, `LAWS.bend`를 적용한 뒤에는 규칙이 유지될 때까지 수정을 반복했다. 벤드는 이 과정에서 버그를 병합하는 것은 수학적으로 불가능하며, 이것이 하나의 정리(theorem)라고 설명했다. 사용자는 `AGENTS.md`에 벤드 사용 지침을 추가한 뒤 AI에 “use Bend”라고 요청할 수 있고, 절대 깨지면 안 되는 조건을 법칙으로 작성하거나 빠른 실행이 필요한 작업의 병렬화를 지시할 수 있다.
벤드는 아직 초기 단계이며, 문제가 발생하면 이슈를 등록해 달라고 안내했다. 현재는 백엔드 작업에 가장 적합하고, 리눅스와 macOS에서 작동한다고 밝혔다. 원문에는 가격, 별도 출시 일정, 고객사 또는 경쟁사 반응에 관한 내용은 포함되지 않았다.