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년 6월 15일 형식적 증명 없이도 차등 테스트는 통하지만, 공통 모드 오류가 함정이다 차등 테스트는 정답을 몰라도 버그를 찾아준다. 문제는 상관관계 있는 실수가 '일치'로 보인다는 점이다. 여기서 사각지대를 찾는 법을 알아본다. n-version-programmingdifferential-testingformal-methodstrust
2026년 6월 14일 테스트는 두 함수가 동등함을 증명할 수 없다. 이것이 가능한 방법이다. N-version programming은 구현체들이 서로 일치한다고 가정한다. 테스트가 왜 부족한지, SMT solver가 어떻게 실제로 동등성을 증명할 수 있는지, 그리고 '충분히 좋음'과 '형식적으로 검증됨' 사이의 경계를 어디에 그어야 하는지 살펴본다. n-version-programmingequivalence-testingformal-methodsverification
