2026년 7월 28일 LLM이 코드의 정당성을 증명할 수는 없지만, 그것을 위한 상용구는 작성할 수 있다 클린룸 검증은 검증 조건을 생성하고 해소하는 것을 요구한다. 여기서 LLM이 주석과 VC 생성을 자동화하여 실제 어려운 증명에 집중할 수 있게 하는 방법을 소개한다. cleanroom-correctnessllmformal-proofsautomation
2026년 7월 8일 LLM은 Rust 코드를 생성할 수 있다. 형식적 증명은 전혀 다른 문제다. 대규모 언어 모델은 놀랄 만큼 훌륭한 Rust 코드를 작성하지만, 형식적 증명을 요청하면 불변 조건을 환각으로 만들어내고 어떤 검증기도 받아들이지 않는 문법을 지어낸다. 이들이 실제로 제대로 하는 것, 실패하는 부분, 그럼에도 불구하고 활용하는 방법을 소개한다. model-checkingllmrustformal-proofs
