6 posts
AutoVerus는 LLM 에이전트 네트워크를 사용해 Rust 코드에 대한 Verus 정합성 증명을 생성하며, SMT 솔버 피드백에 의해 구동되는 생성-수정-디스차지 루프를 통해 90% 이상의 증명 의무를 자동화한다.
형식 검증에서 가장 어려운 부분은 검증기 자체가 아니다. 증명을 작성하는 것이다. 숙련된 Rust 엔지니어에게 Microsoft Research의 SMT 기반 검증기인 Verus를 주면, 오후 한때에 함수에 precondition과 postcondition을 주석으로 달 수 있다.…
대규모 언어 모델은 놀랄 만큼 훌륭한 Rust 코드를 작성하지만, 형식적 증명을 요청하면 불변 조건을 환각으로 만들어내고 어떤 검증기도 받아들이지 않는 문법을 지어낸다. 이들이 실제로 제대로 하는 것, 실패하는 부분, 그럼에도 불구하고 활용하는 방법을 소개한다.
LLM은 컴파일되고 까지 통과하는 Rust 코드를 작성할 수 있다. 하지만 모든 가능한 입력에 대해 코드가 올바르다는 형식적 증명을 믿을 수 있게 작성하는 것은 아직 불가능하다. 문제는 Rust 문법이 아니다. 형식적 검증에서는 무엇을 증명할지 명시하고, 증명을 성립시키는 불변 조건을…
model checking이 며칠간의 프로덕션 런타임을 능가해 concurrency 버그를 찾는 이유, 그리고 자신의 코드에 적용하는 방법.
프로덕션에서 race condition이 떠오르기를 기다리는 건 테스트가 아니다. 성실함으로 위장한 희망이다. 앱을 몇 주씩 돌리고 metrics 대시보드를 지켜봐도, 두 개의 request가 정확히 동일한 cache eviction window에 걸릴 때만 발동하는…
Kani 같은 경계 model checker과 Alloy 같은 관계 모델 탐색기는 일반적인 어서션과 제약 조건으로 속성을 검증할 수 있게 한다. 활성 증명을 포기하는 대신, 학습 곡선은 주가 아닌 시간 단위로 측정된다.
model checker을 사용하기 위해 선형 시간 논리를 배울 필요는 없다. Kani, CBMC, Alloy 같은 도구는 일반적인 어서션과 관계 제약으로 속성을 검증할 수 있게 한다. 활성 속성을 증명하는 능력을 포기하는 대신, 학습 곡선은 주 대신 시간 단위로 측정되며, 대부분의…
Kani 같은 model checking 도구를 사용하면 형식적 증명 대신 단언으로 Rust 속성을 검증할 수 있다. 문제는 루프의 경계가 작지 않을 때 무슨 일이 일어나는지다.
한 줄의 증명도 쓰지 않고 Rust 코드의 정확성을 증명할 수 있다. 이 일을 하는 도구를 model checker라 부르며, 현재 Rust 에 가장 실용적인 것은 AWS 가 개발한 Kani 다. 평범한 Rust 단언을 작성하면 된다. Kani 는 이를 수학적 명제로 변환하고 가능한…
분산 버그는 배포 후 수정 비용이 많이 든다. 모델 검증을 사용하면 구현 코드를 한 줄도 작성하지 않은 상태에서 그 버그를 찾을 수 있다. 다음은 TLA+를 이용한 방법이다.
분산 프로토콜은 단위 테스트할 수 없다. 단위 테스트는 한 대의 머신에서 한 개의 프로세스를 정해진 순서로 실행한다. 당신의 프로토콜은 다섯 대의 머신에서 열 개의 프로세스를 통제할 수 없는 순서로 실행한다. 이 두 현실 사이의 간극이 바로 버그가 서식하는 곳이다. 모델 검증은 그…