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월 5일 한 줄의 증명도 쓰지 않고 Rust 코드의 정확성을 증명할 수 있지만, 상태 공간이 대가다 Kani 같은 model checking 도구를 사용하면 형식적 증명 대신 단언으로 Rust 속성을 검증할 수 있다. 문제는 루프의 경계가 작지 않을 때 무슨 일이 일어나는지다. model-checkingrustverificationformal-methods
2026년 6월 26일 의존성은 디스크의 어떤 파일이든 읽을 수 있다. cap-std는 접근 권한을 요청하게 만든다. Rust 표준 라이브러리는 모든 의존성에 주변 파일 시스템 권한을 부여한다. cap-std는 이를 기능 기반 API로 대체하여 코드가 파일을 열기 전에 해당 경로에 접근할 권리가 있음을 증명하도록 강제한다. capability-based-securityrustcap-stdsandboxing
2026년 6월 22일 타입 검사기가 볼 수 없는 에러 던지기는 이제 그만 던져진 예외는 실패 경로를 타입 시스템에서 감춥니다. 명시적인 에러 반환이 코드를 더 정직하게 만드는 이유, 그리고 삶을 싫어하지 않으면서 이를 도입하는 방법을 알아봅니다. type-level-correctnesserror-handlingtypescriptrust
2026년 6월 21일 Rust newtype는 잘못된 상태를 컴파일 타임에, 아무런 비용 없이 표현 불가능하게 만든다 단일 필드 래퍼 struct가 단 한 바이트의 오버헤드도 추가하지 않고 단위 혼합 버그와 타입 혼란을 잡아낸다. type-level-correctnessrustnewtypeszero-cost-abstractions
2026년 5월 28일 Rust에서 뮤테이션 테스트는 통하지만, 컴파일 시간이 복수한다 cargo-mutants는 코드를 검증하는 척만 하는 테스트를 찾아낸다. Rust에서 뮤테이션 테스트가 어떻게 작동하는지, 무엇을 잡아내는지, 그리고 컴파일 시간 비용이 감당할 만한 가치가 있는지 알아본다. deep-divesmutation-testingrustcargo-mutantstest-quality
2026년 5월 23일 Rust의 Property-Based Test가 당신의 Unit Test가 놓치는 버그를 찾아낸다 Example-based testing은 당신이 생각해낸 입력만 커버한다. Property-based testing은 무작위 데이터를 생성하고, invariant를 검증하며, 실패를 최소한의 counterexample로 축소한다. deep-divesrustproperty-based-testingquickcheckproptest
2026년 5월 21일 Rust 런타임 contracts는 릴리스 빌드에서 오버헤드 없이 사용할 수 있지만, 컴파일러가 대신 해주지는 않는다 Rust는 디버그 assertions를 자동으로 제거하지만, 진정한 design-by-contract는 debug_assert! 이상의 것이 필요하다. 릴리스 바이너리에서 완전히 사라지는 zero-cost runtime contracts를 만드는 방법을 소개한다. deep-divesrustruntime-contractsperformance
