LLMLL은 AI 에이전트가 계약이 붙은 코드의 빈칸을 채우면 컴파일러가 타입을 확인하고 Z3 기반 SMT 검증으로 계약 충족 여부를 판정하는 프로그래밍 언어·검증 파이프라인이다. 제작 측은 코드가 타입에 맞더라도 계약을 위반하면 패치를 적용하지 않는다고 설명한다.

예를 들어 두 계좌의 이체 결과가 총액을 보존해야 한다는 계약을 두면, 받는 계좌에 1을 더 넣는 구현은 타입 검사를 통과해도 사후조건을 만족하지 못해 거부된다. README의 잘못된 구현은 검증 작동을 보여주기 위해 미리 작성한 예시이며, 에이전트가 생성한 결과가 아니다. 이와 같은 속성은 Dafny, Liquid Haskell, F*도 검증할 수 있으며, LLMLL이 내세우는 차이는 에이전트가 계약이 붙은 빈칸을 채우고 컴파일러가 병합 전에 검증하는 작업 흐름이다.

에이전트는 llmll checkout으로 전제조건·사후조건·범위 내 이름을 포함한 타입 지정 ?hole을 받아 코드를 작성한다. llmll patch는 수정된 프로그램을 다시 타입 검사하고 검증한 뒤에만 적용한다. 여러 에이전트는 대화가 아니라 계약을 기준으로 협업하고, 구조화된 JSON-AST 패치를 사용한다. 약한 계약을 찾아내는 검사 기능도 있지만, 계약이 실제로 의도한 동작을 표현하는지까지 보장하지는 않는다.

검증 범위에는 정수 선형 산술, 조건문, 계약이 있는 함수 호출, 비재귀 합 타입, 쌍, 일부 배열·맵 연산과 문자열 리터럴 등이 포함된다. 비선형 산술, 문자열 결합·부분 문자열, 입출력 등은 SMT로 증명되지 않아 계약 검사·속성 기반 테스트·런타임 단언 등으로 처리되며, 결과에는 신뢰 수준이 표시된다. 제작 측은 세 개의 최신 모델이 특정 오류를 유도하도록 만든 테스트 사례에서 30회 중 30회 검증된 구현을 작성했고, 54회 시도에서 잘못된 채움은 없었다고 보고한다. 이는 에이전트가 작성한 코드가 에이전트가 쓰지 않은 계약을 만족했다는 보증에 관한 결과이며, 독립 검증 결과로 제시된 것은 아니다.

비선형 산술에는 실험적 선택 기능인 --leanstral 경로도 있다. Leanstral API 키와 로컬 Lean 4·Mathlib 프로젝트가 필요하며, Lean 커널이 증명서를 확인해 verified-lean 등급을 기록한다. 다만 계약을 Lean 정리로 변환하는 LLMLL의 과정은 여전히 신뢰해야 하고, 모든 검증 의무를 대상으로 한 프로덕션 Lean 검증은 제공되지 않는다.

Docker 이미지는 llmll, z3, liquid-fixpoint를 포함해 별도 Haskell 도구 체인 없이 실행할 수 있다. 소스에서 빌드하려면 GHC 9.4 이상과 Stack 2.9 이상이 필요하고, 증명 단계에는 z3와 liquid-fixpoint도 설치해야 한다. 솔버가 없으면 증명되지 않으며, 소스 설치 경로에서 verify는 종료 코드 3으로 끝나고 patch와 refine은 변경을 적용하지 않는다.

문서와 예제는 프로젝트 저장소, 시작 안내, 전체 언어 명세, 실험 결과 색인에서 확인할 수 있다. 이체 검증의 실행 안내서와 에이전트 패치 과정을 다룬 복구 루프 안내서도 제공한다.