형식 검증 (Formal verification)은 모델을 작성하고 유지 관리하는 비용이 역사적으로 얻는 이득보다 더 컸기 때문에 실제 운영되는 소프트웨어에 적용되는 경우가 드뭅니다. 동반 연구 [1]는 SysMoBench [4]를 더 저렴한 대안으로 확장했습니다. 즉, 실행 중인 시스템에서 캡처된 트레이스 (traces)를 기준으로 명세 (specifications)를 평가하는 방식입니다. 해당 연구는 대규모 언어 모델 (Large Language Models, LLMs)이 명세를 작성할 때, 신뢰성이 언어가 아닌 명세 계약 (specification contract)의 구조에 의해 결정된다는 것을 발견했습니다. 본 논문은 실제 운영 소프트웨어에서 이 두 가지를 모두 평가합니다. 대상은 계산기, 결제 단말기, 결제 프로세서 간의 일치성을 유지해야 하는 실제 레스토랑의 포인트 오브 세일 (Point-of-Sale, POS) 시스템 결제 워크플로우입니다. 우리는 세 가지 결과를 보고합니다. 첫째, 핵심 프로토콜은 정밀하게 기술된 실패 모델 (failure model) 하에서 수동으로 구축된 라인 인용 모델 (line-cited model)과 비교했을 때 정확했습니다. 감사 결과 7개의 실패 처리 공백 (failure-handling gaps)이 발견되었으며, 거의 모두 공통된 근본 원인을 가지고 있었습니다. 이 중 3개는 실제 실행으로 재현되었으며, 이를 해결하는 패치를 모든 실패 게이트 (failure gates)를 활성화한 상태에서 재검증했습니다. 그 후 후속 패치를 통해 재검증 과정 자체에서 노출된 결함을 해결했습니다. 실패 모델의 체계적인 확장 (crash-restart, stale reads, two attempts)은 각각 설계된 대로 조사하려는 윈도우 (windows)를 찾아냈습니다. 둘째, 운영 결제 샌드박스 (payment sandbox)에 대한 단 한 번의 조사로, 라이브 API에 대해 전체 복구 사다리 (recovery ladder)를 도달 불가능하게 만드는 응답 형태의 발산 (response-shape divergence)을 발견했습니다. 에뮬레이터 기반 감사에서는 이를 감지할 수 없었는데, 코드와 에뮬레이터가 동일한 오독을 공유하는 상관된 오라클 실패 (correlated-oracle failure) 때문이었습니다. 셋째, 동반 연구의 핵심 발견은 두 업체에서 제공하는 7개의 모델에 걸쳐 재현되었습니다. 즉, 언어가 아니라 계약 구조 (contract structure)가 LLM이 신뢰성 있게 명세하는 내용을 결정합니다. 이 재현은 절대적인 수준이 아니라 계약의 순서와 실패 분류 체계 (failure taxonomy)에 관한 것입니다. 가장 강력한 모델들만이 코퍼스 천장 (corpus ceiling)에 도달했으며, 더 어려운 작업은 벤치마크가 잃어버렸던 변별력을 회복시켜 주었습니다.