LLMLL의 예시에서는 목적지 잔액에 1을 더하는 잘못된 코드가 잔액 합계를 깨뜨려 검증에 실패한다. 이 코드는 에이전트가 만든 결과가 아니라 검증기가 작동하는 모습을 보이려고 미리 작성한 예시다.
LLMLL은 AI 에이전트가 함수 계약을 만족하는 코드를 작성하도록 설계한 프로그래밍 언어이자 검증 도구다. 에이전트가 만든 코드가 계약에 맞는지 병합 전에 확인하려는 팀에 쓸모가 있다.
LLMLL은 어떤 도구인가?
계약을 함수가 지켜야 할 조건표라고 떠올리면 쉽다. LLMLL에서는 에이전트가 비어 있는 코드 자리인 ?hole을 채우고, 컴파일러가 그 결과가 계약과 타입에 맞는지 확인한다. 에이전트끼리는 대화 대신 계약을 기준으로 작업을 나눈다.
잘못된 코드와 올바른 코드는 어떻게 갈리나?
conserve(from, to, amount)는 이체 뒤 두 잔액을 반환하며, 두 값의 합이 이체 전 잔액 합과 같아야 한다. LLMLL은 SMT(만족 가능성 모듈로 이론) 솔버 Z3를 이용해 두 반환값을 함께 검증한다. 잘못된 구현은 타입에는 맞지만 계약을 깨뜨린다.
# body: (pair (- from amount) (+ to (+ amount 1))) ← type-correct, creates money
$ llmll verify conserve-bad.llmll
error: body verification of 'conserve-bad' failed —
implementation does not satisfy postcondition (constraint #0)
# body: (pair (- from amount) (+ to amount)) ← correct, conserves the sum
$ llmll verify conserve.llmll
✅ conserve.llmll — SAFE (liquid-fixpoint)
이 반례는 솔버가 조건 위반을 찾아낸다는 점을 보여주기 위해 미리 작성됐다. 이 예시에서 에이전트가 잘못된 코드를 생성한 것은 아니다. Dafny, Liquid Haskell, F*도 같은 종류의 속성을 반증할 수 있다고 LLMLL은 설명한다. LLMLL이 내세우는 차이는 검증기 자체의 우월성이 아니라 에이전트가 빈 코드를 받아 수정안을 내고, 검증기가 거부하거나 받아들이는 작업 흐름이다.
실험 결과도 범위를 한정해 읽어야 한다. experiments/minimal-agent/의 보고에 따르면 세 개의 최신 모델이 에이전트가 작성하지 않은 계약을 기준으로 한 시험용 사례에서 검증된 코드를 30회 중 30회 작성했다. 54번의 시도에서 잘못된 채움은 0회였다. 이는 계약에 맞는 코드가 생성됐다는 보증에 관한 근거이지, 에이전트가 코드의 모든 동작을 이해했다는 증거는 아니다.
검증은 무엇을 보장하고 무엇을 남기나?
LLMLL은 코드가 선언한 명세와 일치하는지를 추적하고 함수마다 신뢰 수준을 표시한다. verified는 솔버가 증명한 계약을 뜻하고, asserted는 증명되지 않은 계약을 뜻한다. 검증된 함수가 증명되지 않은 하위 함수에 조용히 기대지 않도록 신뢰 수준을 전달한다.
--weakness-check는 너무 약해 사소한 구현도 통과하는 계약을 찾는다. --cdp는 계약이 잘못된 구현을 얼마나 가려내는지 점수화한다. 두 검사는 계약이 실제 의도와 일치하는지 보장하지 않는다. 엉뚱한 동작을 명세한 계약이라도 잘못된 코드를 잘 걸러내면 검사를 통과할 수 있다.
기본 증명 경로는 Z3와 liquid-fixpoint를 이용하며, 정수 선형 산술을 포함한 제한된 범위에서 함수 본문을 검증한다. 정수의 범위, 잔액 보존, 길이 보존, 배열·맵의 경계와 키 존재 여부, 문자열 리터럴 구별 등이 포함된다. 문자열 결합·부분 문자열·정규식, 재귀 자료형의 페이로드, 비선형 산술인 *, /, mod, 입출력 등은 이 증명 범위를 벗어난다. 이런 경우 계약만 확인하거나 속성 기반 시험, 실행 중 단언으로 대체되며 신뢰 수준에 표시된다.
재귀 함수는 (decreases e) 측정값을 솔버가 증명하면 종료까지 확인한다. 측정값이 없으면 종료 여부가 검증되지 않는다. 이 경우 verify 결과에서 안전 표시가 빠지고 해당 함수가 표시된다.
증명 범위를 벗어난 수식도 확인할 수 있나?
square(n) = n*n의 결과가 0 이상이라는 조건은 비선형 산술이어서 기본 SMT 증명 범위에 들지 않는다. LLMLL은 이 조건을 asserted로 표시한다. 실험 기능인 --leanstral을 선택하면 Leanstral에 증명을 요청하고, Lean 커널과 Mathlib으로 증명을 확인해 verified-lean 등급과 재검증 가능한 .lean 인증서를 기록한다.
$ llmll verify examples/leanstral-demo/square.llmll --trust-report
square: post: asserted # nonlinear: outside the SMT fragment, not proven
$ LLMLL_LEANSTRAL_API_KEY=… llmll verify examples/leanstral-demo/square.llmll \\
--leanstral --leanstral-lean-project ~/proofcheck --trust-report
square: Leanstral proof found, Lean kernel + Mathlib CHECKED
square: post: verified-lean (certificate: square.verified.lean)
인증서는 Lean 커널이 받아들인 증명 항이라 Leanstral을 신뢰하지 않고도 Lean으로 확인할 수 있다. 다만 계약을 Lean 정리로 옮기는 LLMLL의 변환은 여전히 신뢰해야 한다. 이 기능은 실험적이며, Leanstral API 키와 로컬 Lean 4·Mathlib 프로젝트가 필요하다. 모든 증명 의무를 대상으로 한 제품 수준의 Lean 검증은 아직 제공되지 않는다.
직접 사용하려면 무엇이 필요한가?
Docker 이미지에는 llmll, z3, liquid-fixpoint가 포함돼 있어 Haskell 도구 체인 없이 실행할 수 있다. 현재 디렉터리의 파일을 검증하려면 디렉터리를 /work에 연결한다.
# see the SMT refutation of a conservation-breaking fill (no local files needed):
docker run --rm ghcr.io/machunter/llmll verify /opt/llmll/examples/payments-core/conserve-bad.llmll
# verify your own file (mounts the current directory at /work):
docker run --rm -v "$PWD":/work ghcr.io/machunter/llmll verify myfile.llmll
소스에서 빌드하려면 GHC 9.4 이상과 Stack 2.9 이상이 필요하다. 증명 단계에는 z3와 liquid-fixpoint도 필요하다.
cd compiler && stack build
stack exec llmll -- --help
둘 중 하나라도 설치되지 않은 상태에서 소스 빌드 경로로 verify를 실행하면 SOLVER NOT FOUND -- NOTHING WAS PROVEN 경고가 나오고 종료 코드 3으로 끝난다. 이때 patch와 refine도 계약이 붙은 수정을 적용하지 않고 PatchVerifyUnavailable과 종료 코드 3을 반환한다. Docker 이미지에는 솔버가 포함된다.
간단한 예제 확인과 빌드는 다음과 같다.
cd compiler
# Check the example
stack exec llmll -- check ../examples/hangman_sexp/hangman.llmll
# Build a Haskell package in generated/hangman_sexp
stack exec llmll -- build ../examples/hangman_sexp/hangman.llmll -o ../generated/hangman_sexp
# Build from JSON-AST
stack exec llmll -- build ../examples/hangman_json/hangman.ast.json -o ../generated/hangman_json
# Run the generated game
cd ../generated/hangman_json && stack build && stack exec hangman
LLMLL은 사람이 편집하기 좋은 S-표현식 .llmll과 에이전트용 JSON-AST .ast.json을 입력으로 받는다. 두 형식은 같은 추상 구문 트리로 컴파일된다. JSON-AST는 스키마에 맞춘 구조화 입력이다.
도구에는 타입 검사 llmll check, 빈 코드 자리 목록 출력 llmll holes, 속성 기반 시험 llmll test, Haskell 패키지 생성 llmll build, 프로그램 실행 llmll run, 검증 llmll verify, 검증 기록 재생성·확인 llmll replay-artifact, 빈 코드 자리의 타입 추론 llmll typecheck --sketch, 에이전트용 HTTP 인터페이스 llmll serve가 있다.
에이전트 작업 흐름에서는 llmll checkout이 빈 코드 자리를 잠그고 계약과 타입 문맥을 제공한다. llmll patch는 JSON 패치를 적용한 뒤 타입과 SMT 검증을 다시 수행한다. llmll refine은 빈 자리를 채우면서 계약이 붙은 하위 자리로 나누며, 실현 불가능하거나 내용이 없는 하위 계약은 거부한다. 이 저장소는 RFC 6902 JSON-Patch로 구조를 수정하므로 텍스트 병합 충돌을 피하도록 설계됐다.
주요 문서와 실험 결과는 LLMLL 저장소, 시작 안내, 검증 범위 전체표, 실험 목록, Leanstral 데모에서 확인할 수 있다. 저장소는 GPLv3와 LLMLL 런타임 라이브러리 예외를 적용한다.
시험해 보려면 먼저 사용할 코드가 기본 SMT 증명 범위에 들어가는지 확인해야 한다. Leanstral 경로에는 별도 API 키와 Lean 4·Mathlib 프로젝트가 필요하다. 원문은 LLMLL의 가격이나 지원 범위에 관한 별도 정보를 밝히지 않는다.
부록: 원문 예시
](https://github.com/machunter/llmll/blob/main/docs/README.md) is the reading guide to the documentation · [
](https://github.com/machunter/llmll/blob/main/ROADMAP.md) says what has shipped and what is next · [
원문의 "body: (pair (- from amount) (+ to amount)) ← correct, conserves the sum" 대목에 실린 예시다.
](https://github.com/machunter/llmll/blob/main/examples/payments-core/DEMO-RUNBOOK.md) — the composed
](https://github.com/machunter/llmll/blob/main/examples/withdraw-demo/DEMO-RUNBOOK.md) (narrated: [
](https://github.com/machunter/llmll/blob/main/experiments/minimal-agent/SUMMARY.md), three frontier models wrote verified-correct bodies 30 of 30 times on fixtures built to trip them, with 0 wrong fills in 54 attempts. The evidence is for assurance: agent-written code, proved against a contract the agent did not write. The refutation demos in this README and on the blog use scripted wrong versions to show that the check works; the agents in these experiments did not produce them. Every experiment, with its result: [
) and a local Lean 4 + Mathlib project. Production Lean verification across all obligation classes is the deferred
](https://github.com/machunter/llmll/blob/main/examples/leanstral-demo) (
docs/archive/shipped-design-specs/leanstral-demo-spec.md
원문의 "verify your own file (mounts the current directory at /work):" 대목에 실린 예시다.
). Install both to see the refutation. (The Docker image bundles both, so it never hits this.) See [
) even flags a contract so weak that a trivial implementation satisfies it. Its discriminative-power sibling (
), IO — falls back to contract-only checking, property tests, or runtime assertions, each carrying an explicit trust label (full matrix in [
](https://github.com/machunter/llmll/blob/main/LLMLL.md)). Recursion is inside the fragment: with a
](https://github.com/machunter/llmll/blob/main/tools/llmll-driver/README.md) is the RFC-SWARM pipeline driver: 8522 lines across 39 modules, with 55 proved functions and 581 effectful
: unbound variables, unknown functions, unknown operators, and branch type mismatches are hard errors instead of warnings. Without
llmll holes <file> [--deps] [--deps-out FILE]
llmll build-json <file.ast.json> [-o <dir>]
. The program inherits this process's stdin, stdout and stderr, and
llmll verify <file> [--fq-out FILE] [--leanstral] [--leanstral-lean-project DIR] [--leanstral-mock] [--trust-report] [--weakness-check] [--obligations] [--obligation-report] [--spec-coverage] [--strict-verified-core] [--cdp] [--strict-verify] [--proof-artifact FILE]
/sidecar surfaces plus the determinism pins. With
--trust-report --weakness-check --spec-coverage --cdp
llmll serve [--host H] [--port P] [--token T]
llmll checkout <file.ast.json> <pointer> [--multi N]
llmll diverge-report <file.ast.json> <session>
. A fill the solver could not grade (no solver, or no verdict) is listed under
llmll patch <file.ast.json> <patch.json>
llmll refine <file.ast.json> <refine.json>
llmll hub scaffold <template> [--output DIR]
원문의 "Run the generated game" 대목에 실린 예시다.
), all verified; the twin that drops one guard is
: one hole decomposed top-down into a contracted sub-hole tree, every intermediate state
댓글 (0)
로그인하면 이 기사에 내 생각을 남길 수 있어요