프로그램 검증은 소프트웨어의 정확성에 매우 중요하지만, 실제로 완전히 검증된 프로그램을 만드는 것은 여전히 어렵습니다. 본 논문에서는 여러 개의 생성된 프로그램이 동일한 작업 수준 의미론(task-level semantics)을 만족하도록 의도될 때, 구현 구조가 자동화된 검증 가능성(automated verifiability)에 영향을 미치는지 연구합니다. 우리는 Why3를 위한 단계별 LLM 기반 파이프라인인 Diversify2Verify를 제시합니다. 이 시스템은 표현(representation) 특이적 계약을 추론하고, 다양한 재귀 및 명령형 배열/리스트 구현을 생성 및 테스트하며, 유한 검증기 안내 주석 복구(bounded verifier-guided annotation repair)를 통해 검증을 시도합니다. 또한 우리는 정수, 배열, 리스트에 걸친 73개 작업으로 구성된 검증 지향 벤치마크를 구축했으며, 이를 통해 292개의 구현 변형을 얻었습니다. Diversify2Verify는 초기 96개의 아티팩트를 검증하고 두 번의 복구 과정을 거쳐 154개의 아티팩트로 늘려, 아티팩트 수준의 검증률을 32.9%에서 52.7%로 향상시켰습니다. 작업 수준에서는 73개 작업 중 최소 49개 작업에 대해 하나 이상의 변형이 검증되는 결과를 얻었으며, 이는 67.1%의 성공률입니다. 이러한 결과는 작업 동등한 구현들이 검증 가능성 측면에서 상당히 다를 수 있으며, 구현 다양성이 검증 친화적인 아티팩트를 찾는 데 도움이 된다는 것을 보여줍니다.