마팅게일 (Martingale) 기반 방법론은 확률적 프로그램 검증 (probabilistic program verification)의 핵심이지만, 강력한 전역적 비음수성 (strong global non-negativity) 요구 사항은 다루기 쉬운 템플릿 클래스 (template classes)로부터 단순한 증명서 (certificates)를 배제할 수 있습니다. 이 요구 사항을 완화하면 자동 합성 (automated synthesis)을 위한 탐색 공간이 넓어지지만, 확률적 설정 (probabilistic setting)에서 단순한 완화는 건전하지 (unsound) 않습니다. 본 논문에서는 게으른 Streett 슈퍼마팅게일 (lazy Streett supermartingales)과 그 사전식 확장 (lexicographic extension)을 소개하며, 약한 비음수성 (weak non-negativity)을 사용하더라도 모든 유계 지지 분포 (bounded-support distributions)를 포함한 광범위한 샘플링 분포 클래스 하에서 다항식 템플릿 (polynomial templates)을 통해 $\omega$-정규 속성 ($\omega$-regular properties)의 거의 확실한 만족 (almost-sure satisfaction)을 건전하게 증명할 수 있음을 보여줍니다. 이는 기존의 약한 비음수성 방법을 종료 (termination) 문제에서 일반적인 $\omega$-정규 검증으로 확장한 것입니다. 나아가 우리는 1차원 증명서 관점에서 사전식 증명서 (lexicographic certificates)에 대한 구성적 설명 (compositional account)을 제공합니다. 170개의 다항식 확률적 프로그램 벤치마크에 대한 실험 결과, 강력한 비음수성 (strongly non-negative) 베이스라인 대비 검증 성공률이 20.0~23.5 퍼센트 포인트 증가함을 보여줍니다.