aallan/vera

해결하는 문제

LLM은 코드 일관성 유지, 대규모 코드베이스 전반의 불변성 유지, 상태 추론에 어려움을 겪는 경우가 많습니다. 또한 명명 오류가 발생하거나 변수 식별자를 놓치기 쉽습니다. Vera는 변수 이름을 구조적 참조로 대체하고 모든 함수에 대해 명시적이고 검증 가능한 계약을 요구함으로써 이러한 문제를 해결합니다.

작동 방식

Vera는 코드의 정확성을 보장하기 위해 독특한 방식을 사용합니다:

• 구조적 참조: 변수 이름 대신 타입이 지정된 De Bruijn indices (예: @Int.0)를 사용하여 명명 관련 오류를 방지합니다.
• 필수 계약: 모든 함수는 requires (사전 조건), ensures (사후 조건) 및 effects (부작용)를 선언해야 합니다.
• 정적 검증: SMT 솔버 (Z3)가 컴파일 시점에 이러한 계약이 성립하는지 증명하려고 시도합니다.
• 3단계 검증: 계약을 정적으로 증명할 수 없는 경우, 컴파일러는 런타임 가드를 삽입하여 조용한 실패가 발생하기 전에 오류를 포착합니다。
• 에이전트 중심 진단: 오류는 LLM을 위한 지침으로 설계되어, 문제 해결을 위한 근거와 구체적인 코드 예시를 제공합니다.

대상

• LLM 에이전트: 이 언어는 AI 모델이 작성하도록 특별히 최적화되어 있으며, 에이전트 워크플로우에 맞춤화된 문서 (SKILL.md) 및 지침 (AGENTS.md)을 제공합니다.
• AI 기반 시스템을 구축하는 개발자: 모델에 의해 생성된 고신뢰성 코드가 필요한 개발자.

주요 특징

• CLI, 브라우저 또는 WASI Preview 2 호스트에서 실행하기 위해 WebAssembly로 컴파일됩니다.
• <Inference> 또는 <Http>와 같은 부작용을 추적하기 위한 명시적 이펙트 시스템을 특징으로 합니다.
• 에디터 지원을 위한 Language Server Protocol (LSP)을 포함합니다.
• 전통적인 언어와 비교하여 Vera를 작성하는 모델의 높은 성공률을 보여주는 벤치마크 (VeraBench)를 포함합니다.