Bend: a fast language that blocks AI mistakes via proof

3줄 요약

1. Victor Taelin이 이끄는 팀이 2026년 9월 17일 Bend 2를 공개했다. 공식 사이트는 이 언어를 “증명으로 AI의 실수를 막는 빠른 언어"로 소개하고, C의 속도와 CUDA의 병렬성, Lean의 증명, Python의 문법을 한 언어로 제공하겠다고 했다.
2. Bend 2는 두 개의 파일로 AI의 실수를 막는다. 사람이 LAWS.bend에 앱이 어겨서는 안 되는 규칙을 적으면, AI는 코드를 고칠 때마다 그 규칙이 여전히 성립한다는 증명을 PROOF.bend에 써야 한다. 증명 검사에 실패한 변경은 커밋할 수 없다.
3. 사이트는 Apple M4 Max에서 잰 벤치마크로 속도를 제시했다. 라이프 게임 벤치마크에서 Bend는 1코어로 7.80초가 걸려 C의 6.78초와 비슷했고, 16코어에서는 0.65초, GPU에서는 0.06초였다. 제네릭 인스턴스화 3,200개를 검사하는 데 Lean은 19.2초가 걸렸고 Bend는 0.38초가 걸렸다.

Bend 2가 내건 전제

사이트의 첫 문단은 이 언어가 왜 필요한지부터 설명한다.

AGI 이후의 경제에서 사람은 언젠가 코드를 쓰지도 읽지도 않게 될 것이다. 그래도 우리를 둘러싼 세상을 만드는 AI에게 우리가 원하는 것을 모호함 없이 전달할 방법은 여전히 필요하다.

사이트는 그 방법으로 세 가지를 제시했다. 법칙(law)을 쓰면 자연어보다 훨씬 정밀하게 의도를 표현할 수 있고, 증명(proof)으로 AI가 프롬프트를 올바르게 구현했는지 검증할 수 있으며, 빠른 컴파일러가 그 코드를 제 속도로 실행한다. 사이트는 이 설명 끝에 “그것이 Bend이고, 그 외에는 아무것도 없다"고 덧붙였다.

Bend 1은 2024년 5월에 처음 공개되었다. 그때의 Bend는 HVM2 런타임으로 Python 풍 코드를 병렬 실행하는 언어였다. README에 따르면 Bend 2는 새 언어이며, Bend 1 프로그램과 HVM은 Bend 2에서 쓸 수 없다. Bend 2는 프로그램을 C 파일 하나로 컴파일한다. 지원하는 타깃은 C, Metal, CUDA, JavaScript다.

Taelin은 X의 발표 글에서 증명 검사를 “대형 AI 연구소들이 나비에-스토크스 같은 미해결 수학 문제를 풀 때 쓴 기법"이라고 소개했다. 리포는 bendlang/bend이고 Apache-2.0 라이선스로 공개되어 있다.¹

설치하고 에이전트에게 알리기

사이트는 설치부터 사용까지를 세 단계로 안내한다. 첫 단계에서는 설치 스크립트를 실행한다.

curl -fsSL https://bend-lang.com/install.sh | sh

두 번째 단계는 에이전트의 AGENTS.md에 아래 네 줄을 추가하는 것이다. Bend를 쓸 때는 bend guide로 언어를 익히고, 중요한 규칙은 LAWS.bend에 적고, 커밋 전에 bend PROOF.bend를 실행하고, 가능하면 코드를 병렬화하라는 내용이다.

When using Bend:
- run `bend guide` to learn it
- use `LAWS.bend` to keep important rules
- run `bend PROOF.bend` before committing
- parallelize the code whenever possible

그다음에는 에이전트에게 “use Bend"라고 말하기만 하면 된다고 한다. 세 번째 단계의 조언은 이렇다. 절대로 어겨서는 안 되는 규칙이 있으면 에이전트에게 그 규칙을 법칙으로 쓰게 하라. 실행 속도가 중요한 코드는 병렬화하게 하라. 문제가 생기면 에이전트에게 이슈를 등록하게 하라.

bend guide는 언어 전체를 설명한 GUIDE.md를 출력한다. 사이트는 Bend가 백엔드 작업에서, 그리고 Linux와 macOS에서 가장 잘 동작한다고 밝혔다. README에 따르면 Windows는 지원하지 않고 WSL에서는 동작한다.

실행 속도

사이트의 설명에 따르면 Bend는 네이티브 코드로 컴파일된다. 1코어에서는 C와 거의 같은 속도로 실행되고, 같은 바이너리를 16코어나 GPU에서 실행하면 1코어보다 최대 100배 빨라진다고 한다.² README는 강한 타입과 순수성, 선형성 덕분에 1코어에서 손으로 쓴 C만큼 빠른 실행 파일을 만들 수 있다고 설명했다. 목표는 CPU에서 C만큼, GPU에서 CUDA만큼 빠른 것이다.

실행 속도 벤치마크. Apple M4 Max, 단위는 초이며 낮을수록 빠르다. 출처: bendlang/bend 리포(Apache-2.0)

사이트의 차트는 열여섯 개 벤치마크를 번갈아 보여준다. 전체 수치는 다음과 같다. 괄호 안의 배수는 Bend 1코어 대비 속도 향상이다.³

1코어 Bend는 트리 행렬 곱 하나에서만 C보다 빨랐다. 열여섯 개 벤치마크에서 1코어 Bend의 실행 시간 중앙값은 C의 1.21배였다. C와 거의 차이가 없었던 벤치마크는 k-평균과 지형 생성으로, 둘 다 실행 시간 차이가 1.2% 이하였다. 반대로 해시맵은 C보다 4.4배, 렉서는 2.1배 오래 걸렸다. TypeScript나 Lean과 비교하면 사정이 다르다. 1코어 Bend는 열여섯 개 가운데 열세 개 벤치마크에서 TypeScript보다 빨랐고, Lean과 비교해도 열세 개에서 빨랐다.

16코어로 실행하면 Bend는 1코어보다 7.6배에서 12배 빨라졌다. 16코어 Bend는 열여섯 개 벤치마크 모두에서 1코어 C보다 빨랐다.

GPU에서 얻은 속도 향상은 벤치마크마다 크게 달랐다. 라이프 게임이 124배로 향상이 가장 컸고, n-체 시뮬레이션과 만델브로 집합도 각각 98배와 78배 빨라졌다. 렉서가 GPU에서 얻은 향상은 2.0배였다. GPU가 16코어보다 느린 벤치마크도 있었다. 해시맵과 렉서, n-퀸, 기호 회귀가 그렇고, 트리 행렬 곱은 GPU와 16코어의 실행 시간이 0.23초로 같았다.

증명 검사 속도

사이트는 검사 속도도 따로 강조했다. Bend의 타입 검사기는 Lean이나 Rocq처럼 증명 검사기다. 그런 도구는 중간 규모 코드베이스를 검사하는 데 몇 분씩 걸리기도 하는데, Bend는 길어도 1초면 끝나므로 AI 에이전트가 코드를 바꿀 때마다 검사할 수 있다고 한다. README가 밝힌 목표는 모든 증명 보조기보다 몇 자릿수 빠른 것이다.

증명 검사 속도 벤치마크. Apple M4 Max, 단위는 초이며 낮을수록 빠르다. 출처: bendlang/bend 리포(Apache-2.0)

증명 3,200개를 검사하는 세 번째 벤치마크에서는 Lean도 Isabelle, Agda처럼 5분 안에 검사를 끝내지 못했다. Rocq는 9.53초, Bend는 0.83초였다. Bend와 다른 도구의 검사 시간 차이가 가장 작았던 벤치마크는 smalltt 트리 400개였다. Lean과 Rocq는 1.34초, Bend는 0.61초였다.⁴

Taelin은 해커 뉴스 댓글에서 대규모 검증 프로그램이 Bend에서 훨씬 빠를 이유를 이렇게 설명했다. Bend는 모든 것을 명시적으로 적는 언어라서 전술(tactic)이 없고, 컴파일 시점에 탐색을 전혀 하지 않는다. 그는 “언제나 그렇듯, 컴퓨터가 하는 일이 적을수록 프로그램은 더 빨리 실행된다"고 했다.

스레드 없이 병렬화한다

병렬화 방식에 대한 사이트의 설명은 짧다. 스레드도, 락도, 직접 작성할 커널도 필요 없다. 작업을 두 개의 재귀 호출로 분할해 작성하면, Bend가 그런 호출들을 사용할 수 있는 코어 전체에 분배한다. 계산이 끝나면 결과를 합친다.

pow2(20)이 재귀 호출을 늘려 GPU 코어 4,096개에 호출을 하나씩 할당한 뒤 결과를 합치는 과정. 출처: bendlang/bend 리포(Apache-2.0)

README에 실린 pow2 예제는 깊이가 d인 트리를 만들고, 각 잎의 값을 1로 정한다. 그 값을 모두 더하면 2의 d제곱이 된다. 함수 이름 뒤에 !를 붙여 호출하면 그 함수가 GPU에서 실행된다.

import Base

# Computes 2^d in parallel: a tree of d levels, one leaf per unit.
def pow2(+d: Nat) -> U32:
  match d:
    case 0n:
      1
    case 1n+p:
      a b = pow2(p) pow2(p)
      (a + b : U32)

# Runs pow2 on the GPU, via `!`.
def main() -> IO(Unit):
  result = pow2!(20n)
  IO.print(U32.show(result))

지금의 스케줄러는 단순하다. Taelin의 해커 뉴스 댓글에 따르면 현재 스케줄러는 이진 재귀 호출을 CPU나 GPU의 모든 코어에 할당해 실행한다. Taelin은 더 유연한 작업 훔치기(task stealing) 큐를 도입하고 싶다고 했다. 그러나 GPU에서는 스레드 사이의 경합 때문에 성능이 크게 떨어져서, 지금은 현재 방식이 가장 낫다고 설명했다. README도 병렬화하려면 각 호출의 계산량이 비슷해야 한다고 밝히며, 더 유연한 병렬화는 나중에 추가하겠다고 했다.

LAWS.bend로 규칙을 강제한다

사이트는 이 기능을 가장 길게 설명했다. 읽지도 않은 코드를 어떻게 믿을 수 있느냐는 질문을 던지고, 증명을 요구하면 된다고 답한다. LAWS.bend는 법칙을 선언하는 파일이다. 사이트에 따르면 법칙을 선언한 뒤에는 어떤 AI도 그 법칙을 어기는 코드를 배포할 수 없다.

작은 게임 하나가 이 과정을 보여준다. 이 게임에는 “이길 수 없다"는 법칙 하나가 있다. 플레이어는 깃발을 잡아야 이기는데, 깃발이 있는 방은 벽으로 막혀 있다.

법칙: 이길 수 없다. 지금까지는 잘 동작한다. 출처: bendlang/bend 리포(Apache-2.0)

이 상태에서 Claude에게 새 기능을 요청한다. “Claude, 보드의 가장자리가 반대편과 이어지게 해 줘.”

LAWS.bend가 없을 때. 법칙이 위반되었고, AI의 실수가 병합되었다. 출처: bendlang/bend 리포(Apache-2.0)

LAWS.bend가 있을 때. 법칙이 유지되었고, AI의 실수가 차단되었다. 출처: bendlang/bend 리포(Apache-2.0)

LAWS.bend가 없을 때는 버그가 그대로 배포되었다. LAWS.bend가 있을 때 AI는 법칙이 성립한다는 증명을 만들어 낼 때까지 재시도해야 했고, 그 과정에서 반대편 가장자리에 벽을 세웠다.⁵ README는 AI가 벽 대신 깃발을 옮기거나, 방에 들어가면 죽게 만들 수도 있었다고 설명했다. AI가 할 수 없는 일은 법칙을 어기는 코드를 커밋하는 것 하나뿐이고, 컴파일러가 그것을 강제한다고 한다.

이 게임에 적용된 법칙은 어떤 이동 순서로 게임을 처음부터 재생해도 승리 상태가 되지 않는다고 선언한다. 증명은 AI가 작성한다.

# LAWS.bend
law you_cant_win:                           # "winning is impossible"
  for moves: List<Game.Move>                # any sequence of moves
  board = Game.replay(Game.start(), moves)  # replayed from the start
  {Game.is_won(board) == False{} : Bool}    # never leads to victory

# PROOF.bend
def Laws.you_cant_win(moves):
  # ... written by the AI

README는 법칙의 예로 다섯 가지를 들었다.

• 모든 잔액의 합은 0이어야 한다.
• 플레이어는 단단한 벽을 통과할 수 없다.
• list_sort()는 항상 오름차순으로 정렬된 수를 반환해야 한다.
• array_set()은 범위 밖의 인덱스로 호출되어서는 안 된다.
• 게임에서 이기는 것은 불가능하다.

README는 “글로 적을 수 있는 것이라면 무엇이든 법칙이 될 수 있다"고 했다. 사용법도 간단하다고 한다. AI에게 앱의 규칙을 LAWS.bend에 형식화하게 하고, 코드를 고친 뒤에는 bend PROOF.bend를 실행하게 하면 된다. 사람이 LAWS.bend를 직접 고쳐도 된다.

Bend에서 법칙은 정리에 해당하고, 증명은 평범한 함수 정의로 작성한다. README는 “x에 0을 더하면 x"라는 법칙과 그 증명을 예로 들었다. 증명에서는 x에 대한 귀납법을 쓰고, 단계마다 %로 식을 한 번씩 다시 쓴다.

# CLAIM: for every nat x, x + 0 equals x.
law add_zero:
  for x: Nat
  {Nat.add(x, 0n) == x : Nat}

# PROOF: induction on `x`, one rewrite (`%`) per step.
def add_zero(x):
  match x:
    case 0n:
      {==}
    case 1n+xp:
      %add_zero(xp) : {1n+Nat.add(xp, 0n) == 1n+_ : Nat}
      {==}

사이트는 LAWS.bend를 “증명이 뒷받침하는 AGENTS.md“라고 요약했다. “실수하지 마"라는 지시가 이제 타입 검사를 받는다는 뜻이다. 사이트 하단에는 같은 게임의 라이브 데모가 있다. 방문자는 WASD로 플레이어를 움직일 수 있다. 이길 수 없다는 것을 확인하면 아래 입력창에서 AI에게 게임 수정을 요청할 수 있다. 사이트는 무엇을 요청해도 Bend가 법칙을 지킨다고 설명하며, 방문자에게 이 게임에서 이겨 보라고 권한다.

README가 밝힌 한계

사이트는 “Bend는 아직 발전 중이다. 버그를 예상하고 제보해 달라"는 문장으로 끝난다. README는 이보다 구체적으로 서른한 가지 한계를 목록으로 적었다. 그 가운데 주요 항목을 옮긴다.

• 모든 것에 타입 주석을 달아야 하고 타입 추론이 없어서 코드가 장황하다.
• 타입 클래스와 트레이트가 없고, 컴파일 타임 템플릿을 제외하면 매크로도 없다.
• 전술과 증명 탐색이 없어서 정리를 증명하는 데 품이 더 든다.
• 값이 아핀(affine)이라서 클로저와 배열을 공유할 수 없다.⁶
• 재귀는 반드시 종료해야 한다. @unsafe나 def f?(..)를 쓰면 종료 검사를 끌 수 있다.
• 수 타입은 Nat, U32, F32뿐이다. F32는 공리로 다루기 때문에 부동소수점에 관해서는 아무것도 증명할 수 없다.
• 문자열이 문자의 연결 리스트라서 텍스트 처리가 느리다.
• TLS와 HTTP 라이브러리, JSON, 정규식이 아직 없다.
• JavaScript 타깃은 1코어에서만 실행되고 그래픽과 오디오를 지원하지 않는다.
• 네이티브 컴파일은 clang, CUDA, Metal을 거치기 때문에 느리다. 빠르게 개발하려면 JavaScript 타깃을 쓰라고 권한다.
• 컴파일러 코드의 99%는 AI가 썼다. 커널은 여기서 제외되며, 컴파일러에 대한 감사는 아직 끝나지 않았다.
• 검사기 자체에는 증명이 없어서 버그가 있을 수 있다. --verdict 옵션은 증명된 커널을 쓴다.
• 패키지 허브에는 아직 이름과 버전, 계정, 검색이 없고, 패키지는 해시로 식별한다.
• 오류 메시지가 간결하고 디버거와 프로파일러, REPL이 없다.

README는 이 가운데 대부분을 개선하는 중이라고 덧붙였다.

가장 흥미로운 지점

읽으면서 가장 의외였던 것은 Bend가 증명을 쓰기 쉽게 만드는 방향을 택하지 않았다는 점이다. Lean과 Rocq는 전술과 자동 탐색을 제공해 사람이 증명을 덜 쓰도록 돕는다. Bend는 그런 기능을 모두 빼고, 증명의 모든 단계를 명시적으로 적게 했다. Taelin은 해커 뉴스 댓글에서 이 선택을 이렇게 설명했다.

이것은 트레이드오프다. 그 대가로 Bend 코드는 Lean보다 훨씬 장황하고, Bend로 증명을 쓰는 일은 더 고되다. 나는 이것이 옳은 트레이드오프라고 본다. 증명은 AI가 쓰고 AI의 시간은 싸지만, 버그는 사람의 시간을 쓰게 만들고 사람의 시간은 비싸기 때문이다.

사람 대신 AI가 증명을 쓰면, 증명 보조기에 요구되는 성질도 달라진다. 사람에게는 적게 써도 되는 언어가 편하다. 반면 코드를 고칠 때마다 검사를 돌리는 에이전트에게는 1초 안에 검사를 끝내는 언어가 편하다. Bend는 검사가 빠른 언어를 택했다. Lean과 비교할 수 있는 세 벤치마크에서 Bend는 2.2배에서 122배 빨랐고, Taelin은 대규모 검증 프로그램에서 Bend가 빠른 이유도 이 선택에서 찾았다.

눈에 띈 점이 하나 더 있다. AI의 실수를 막겠다는 언어인데, README에 따르면 이 언어의 컴파일러는 99%를 AI가 작성했다. Taelin은 컴파일러와 런타임, 커널을 자신이 설계했다고 했다. 커널은 사람이 폭넓게 감사했다고도 설명했다. 게다가 README에 따르면 --verdict 옵션이 쓰는 커널은 Lean으로 형식화하고 증명까지 마쳤다. 코드의 대부분을 AI가 썼더라도, 사용자가 믿어야 하는 부분은 그 작은 커널 하나로 줄어든다. Bend가 사용자에게 제안하는 방식을 Bend 자신에게도 적용한 셈이다.

출처

Bend 공식 사이트. Victor Taelin과 Bend 팀, 2026년 9월 17일 공개.

원문: https://bend-lang.com/

함께 참고한 자료

• GitHub README: https://github.com/bendlang/bend
• Taelin의 X 발표 글: https://x.com/VictorTaelin/status/2100681226143092875
• 해커 뉴스 토론: https://news.ycombinator.com/item?id=49746163

본문의 GIF는 모두 bendlang/bend 리포의 media/ 디렉토리에서 가져왔으며 리포 라이선스는 Apache-2.0이다. 커버 이미지는 game_bug.gif와 game_law_kept.gif의 마지막 프레임을 나란히 이어 붙여 만들었다.