Bend: 증명으로 AI 실수를 막고 GPU에서 도는 언어

Who Should Read

코딩 에이전트가 만든 코드를 읽지 않고 믿어도 되는지 고민하는 백엔드 개발자

Core Mechanics

• 규칙을 어기면 머지가 막힌다
  • LAWS.bend에 '절대 깨지면 안 되는 규칙(law)'을 선언한다.
  • AI는 PROOF.bend에 그 규칙이 성립한다는 증명을 써야 하고, 못 쓰면 코드가 막힌다.
  • 사이트는 이를 'AGENTS.md에 증명을 붙인 것'이라고 소개한다.
• 데모는 보드 게임 지키기다
  • 규칙은 '어떤 이동 순서로도 승리할 수 없다'이다.
  • 'Claude, 보드가 이어지게 해줘'를 시키면 LAWS.bend 없이는 버그가 머지됐다.
  • LAWS.bend가 있으면 AI가 벽을 세우고 규칙이 성립함을 증명할 때까지 재시도했다.
• 타입 체커가 곧 증명 검사기다
  • Lean·Rocq처럼 증명 검사기이지만 중간 규모 코드베이스도 최대 1초라고 한다.
  • 원문은 Lean류가 같은 규모에서 몇 분 걸릴 수 있다고 쓴다.
  • 그래서 에이전트가 변경마다 검사할 수 있다는 주장이다.
• 속도는 네이티브 코드와 GPU에서 나온다
  • 코어 1개에서 C에 거의 근접하다고 한다.
  • 같은 바이너리가 16코어나 GPU에서 코어 1개 대비 최대 100배 빠르다고 한다.
  • 스레드·락·커널 없이 작업을 둘로 나누면 가능한 모든 코어에 자동 분산된다.

Community Reactions

• 증명 라이브러리가 얇아 준비 비용이 크다는 경험
  • 캘린더 크론잡을 포팅해 봤더니 거의 성공했다는 경험이 있었다.
  • Claude가 Base에 덧셈 교환법칙 하나뿐이라, 163줄 PROOF.bend 중 약 60줄이 기초 사실 증명이었다고 불평했다고 한다.
  • '원하던 겹침 없음 규칙'은 정렬 정확성부터 증명해야 해서 쓰지 못했다고 한다.
• AI가 규칙 자체를 고쳐 버린다는 의견
  • 새 기능에 맞추려고 law를 수정해 버려 의미가 없어진다는 경험이 있었다.
  • 일부 규칙은 동결해야 하니 판단은 여전히 사람 몫이라는 의견이다.
  • 에이전트가 비합리적인 짓을 할 때마다 CI에 증명류 검사를 추가해 성공했다는 경험도 있었다.
• 데모에서 토큰만 태웠다는 경험
  • 간단한 기능을 시켰더니 'laws broken' 루프로 10만 토큰 넘게 썼다는 경험이 있었다.
  • 50만 토큰을 쓴 뒤 API 키가 레이트 리밋에 걸려 루프가 끊겼다고 한다.
  • 스페이스바로 보드 뒤집기를 시켰더니 결승선이 2개인 대칭 보드로 땜질했다고 한다.
• 증명 대상이 틀리면 소용없다는 반론
  • 요구사항을 증명 목표로 옮기는 과정에도 코딩과 버그가 있다는 의견이다.
  • law를 결국 AI가 써야 해서 틀릴 수 있다는 의견도 있었다.
  • 정지 문제를 근거로 'AI 실수를 막는다'는 표현이 과하다는 의견, 리포에 커밋 기록이 없어 신뢰하기 어렵다는 의견도 나왔다.

How to Apply

• 오늘 AGENTS.md에 규칙 4줄 시험해 보기
  • 작은 사이드 프로젝트에 install.sh로 Bend를 설치하라.
  • AGENTS.md에 원문의 4줄을 붙이고 'use Bend'라고 시켜 보라.
  • 절대 깨지면 안 되는 규칙 하나만 LAWS.bend에 쓰게 하라.
• 불변식을 먼저 한 줄 문장으로 뽑기
• law 파일은 사람이 승인하게 하기
  • 에이전트가 law를 수정한 diff는 반드시 사람이 리뷰하라.
  • 핵심 규칙은 동결 목록으로 따로 관리하라.
  • 커밋 전 bend PROOF.bend를 CI에 넣어 실패하면 막아라.
• 재시도 토큰 상한 걸기
  • 에이전트 루프에 최대 재시도 횟수와 토큰 예산을 설정하라.
  • 한도에 닿으면 멈추고 사람에게 규칙 완화 여부를 묻게 하라.
  • 데모에서 laws broken 루프로 토큰이 크게 소모됐다는 보고를 참고해 한도를 잡아라.

Try It

# Claude Code 또는 AGENTS.md가 있는 프로젝트 루트에서 실행 (먼저 설치: curl -fsSL https://bend-lang.com/install.sh | sh)

AGENTS.md에 아래 내용을 추가해 줘:
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. 이 프로젝트에서 절대 깨지면 안 되는 규칙은 {{불변식 한 문장}}이야. 이걸 LAWS.bend에 law로 쓰고, PROOF.bend에서 증명한 뒤 bend PROOF.bend가 통과하는지 알려줘.

이어서 해 볼 것: {{새 기능}}을 추가시켜 보고 law가 깨질 때 에이전트가 law를 고치는지 코드를 고치는지 확인해 봐.

Terminology

관련 논문

• 같은 시뮬레이션, 다른 근거: 도구 출력을 파일로 넘기면 LLM 에이전트 정확도가 어디서 깎이나

  긴 툴 출력을 파일로 넘기자 GPT-5.1은 정확도 11.3%p 하락, 정식 출력 지정하니 회복

• 가짜 뉴스가 진짜 폭락을: LLM 트레이딩 에이전트 대상 정보 주입 공격

  가짜 헤드라인 한 줄로 LLM 트레이딩 에이전트 62%를 조종했다(프롬프트 주입은 14%)

• Harness Engineering 101: LLM은 뇌, harness는 몸

  에이전트는 JSON 배열을 관리하는 루프이고, 16개 챕터로 직접 만들어 본다

• Harness²: 에이전트 harness를 스스로 고쳐 쓰는 재귀 최적화 프레임워크

  모델은 고정하고 harness를 재귀로 고쳤더니 벤치마크 점수가 최대 11.8%p 올랐다

• 해고된 Savannah 경찰관, ICE 요원 남편에게 Flock 계정 공유

  경찰관이 Flock 계정을 남편(ICE 요원)에게 공유했고, 감사에서 983건 검색이 드러나 해고됐다

• tmux와 Claude Code: 세션, send-keys, 그리고 한계선

  tmux로 Claude Code 여러 개를 돌리면 편하지만 에이전트 4개쯤에서 한계가 온다

• Hybrid Reasoning Agents: 잠재 공간에서 생각하고 텍스트로 행동하는 LLM 에이전트

  잠재 공간 추론과 텍스트 도구 호출을 섞었더니 성능 10.4%↑, 토큰 최대 54.7%↓

Related Resources

• https://bend-lang.com/
• https://github.com/bendlang/bend/blob/main/guide/GUIDE.md
• https://code-contracts.cc/
• https://www.star-history.com/?repos=bendlang%2Fbend