aallan/vera

해결하는 문제

모델은 규모가 커질수록 일관성을 유지하는 데 어려움을 겪고, 상태에 대한 추론과 변수 이름 관리에 어려움을 겪으며, 이로 인해 이름 관련 오류가 발생하고 값의 추적을 잃게 됩니다. Vera는 대규모 언어 모델이 코드를 작성하기 위해 특별히 설계된 프로그래밍 언어로, 전통적인 변수 이름 대신 구조적 참조를 사용하고, 코드가 기계적으로 검증 가능하도록 계약을 필수적으로 만듭니다.

작동 방식

Vera는 변수 이름을 타입이 지정된 슬롯 참조(예: @Int.0는 최신 정수 바인딩)로 대체합니다. SMT 솔버(Z3)를 사용하여 모든 호출 지점에서 사전 조건(requires)과 사후 조건(ensures)을 정적 증명합니다. 언어는 기본적으로 순수하며, 효과(예: <Http> 또는 <Inference>)는 함수 시그니처에서 명시적으로 선언해야 합니다. 프로그램은 WebAssembly로 컴파일되어 명령줄, 브라우저, 또는 WASI Preview 2 컴포넌트에서 실행할 수 있습니다.

대상 사용자

코드의 주요 작성자로서 AI 에이전트와 LLM을 사용하는 사람, 그리고 모델이 이름 충돌 없이 쉽게 생성할 수 있고, 형식적으로 검증되며 안전한 코드를 원하는 개발자.

주요 특징

• 타입이 지정된 슬롯 참조: 변수 이름 대신 구조적 참조를 사용하여 이름 오류를 제거합니다.
• 필수 계약: 모든 함수는 컴파일러가 Z3를 통해 정적으로 증명하는 사전 조건과 사후 조건을 선언해야 합니다.
• 명시적 효과 타이핑: 부작용은 시그니처에서 명시적으로 타입 지정되어 허가되지 않은 작업을 방지합니다.
• 에이전트 최적화 진단: 컴파일러 오류는 모델을 위한 지침으로 작성되며, 근거와 구체적인 수정 예제를 제공합니다.
• 설계부터 보안: 문자열의 원천에 대한 규칙을 타입 체커 수준에서 강제하여 SQL 인젝션과 같은 일반적인 취약점을 방지합니다.
• 다중 타겟 컴파일: CLI, 브라우저, WASI 0.2 호스트에서 실행 가능한 WebAssembly로 컴파일됩니다.