2026년 7월 9일 AutoVerus는 40시간의 증명 작성을 3회의 LLM 호출로 만든다. 비결은 포기할 때를 아는 것이다. AutoVerus는 LLM 에이전트 네트워크를 사용해 Rust 코드에 대한 Verus 정합성 증명을 생성하며, SMT 솔버 피드백에 의해 구동되는 생성-수정-디스차지 루프를 통해 90% 이상의 증명 의무를 자동화한다. model-checkingautoverusrustverification
2026년 7월 8일 LLM은 Rust 코드를 생성할 수 있다. 형식적 증명은 전혀 다른 문제다. 대규모 언어 모델은 놀랄 만큼 훌륭한 Rust 코드를 작성하지만, 형식적 증명을 요청하면 불변 조건을 환각으로 만들어내고 어떤 검증기도 받아들이지 않는 문법을 지어낸다. 이들이 실제로 제대로 하는 것, 실패하는 부분, 그럼에도 불구하고 활용하는 방법을 소개한다. model-checkingllmrustformal-proofs
2026년 7월 7일 race condition이 나타나기를 기다리는 것은 끔찍한 테스트 전략이다 model checking이 며칠간의 프로덕션 런타임을 능가해 concurrency 버그를 찾는 이유, 그리고 자신의 코드에 적용하는 방법. model-checkingrace-conditionsconcurrencytesting
2026년 7월 6일 시간 논리를 배우지 않고도 코드를 model checking할 수 있다 Kani 같은 경계 model checker과 Alloy 같은 관계 모델 탐색기는 일반적인 어서션과 제약 조건으로 속성을 검증할 수 있게 한다. 활성 증명을 포기하는 대신, 학습 곡선은 주가 아닌 시간 단위로 측정된다. model-checkingtemporal-logicformal-methodsverification
2026년 7월 5일 한 줄의 증명도 쓰지 않고 Rust 코드의 정확성을 증명할 수 있지만, 상태 공간이 대가다 Kani 같은 model checking 도구를 사용하면 형식적 증명 대신 단언으로 Rust 속성을 검증할 수 있다. 문제는 루프의 경계가 작지 않을 때 무슨 일이 일어나는지다. model-checkingrustverificationformal-methods
2026년 7월 4일 분산 프로토콜은 단위 테스트할 수 없지만, 모델 검증은 할 수 있다 분산 버그는 배포 후 수정 비용이 많이 든다. 모델 검증을 사용하면 구현 코드를 한 줄도 작성하지 않은 상태에서 그 버그를 찾을 수 있다. 다음은 TLA+를 이용한 방법이다. model-checkingdistributed-systemstlaplusprotocol-design
