---
name: maintain-formal-verification-skill
description: "코드가 변경된 후 프로젝트의 형식 검증을 코드와 다시 정렬하세요: 검증된 코드를 터치한 커밋을 찾고, 모델, 하니스 또는 속성을 지금 코드를 설명하도록 업데이트하고, 다시 실행하고, 각 실패가 검증의 드리프트인지 코드의 버그인지 말하세요. /maintain-formal-verification-skill, \"is the model still true to the code\", 또는 검증된 코드를 터치했지만 다시 확인하지 않은 병합 및 리팩토링 후에 사용하세요."
disable-model-invocation: true
---

# Maintain a formal verification skill

형식 검사는 그것이 설명하는 것의 속성을 증명합니다. 코드가 변경되고 검증이 변경되지 않으면 검사는 더 이상 존재하지 않는 코드를 설명하는 동안 통과를 계속할 수 있습니다. 그 통과는 증명처럼 보이기 때문에 위험한 경우입니다. 이 스킬은 `/create-formal-verification-skill`이 생성한 verify 스킬 또는 명명된 코드에 대해 모델 체커, 증명기 또는 코드 레벨 검증기를 실행하는 모든 프로젝트 로컬 스킬의 유지보수 루프입니다. 프로젝트 로컬 스킬은 에이전트가 해당 스킬을 사용하는 동안 만드는 변경을 처리합니다. 이 스킬은 그것을 건너뛴 변경을 처리합니다: 병합, 스킬 없이 수행된 편집, 많은 커밋에 걸쳐 쌓이는 드리프트.

## 결과

각 검사에 하나의 결과를 제공하고, 어느 것인지 말하세요:

- **in sync (동기화됨)**: 마지막 동기화 이후 변경 사항이 검사가 설명하는 것을 변경하지 않으며, 검사가 통과합니다.
- **updated (업데이트됨)**: 코드가 변경되었고, 검증이 이제 새 코드를 설명하며, 검사가 통과합니다.
- **bug (버그)**: 검증이 현재 코드를 설명하고, 코드가 속성을 위반합니다. 이것은 코드에 대한 발견 사항입니다. 드리프트가 아닙니다.
- **blocked (차단됨)**: 검사를 다시 정렬하거나 실행할 수 없었습니다. 정확히 왜인지 말하세요.

검사는 updated이면서 bug일 수 있습니다: 업데이트가 검증을 다시 코드를 설명하게 만들고, 그런 다음 속성이 그것에 대해 실패합니다.

## 편집 범위

검증만 편집하세요: 모델, 하니스, 속성 파일, 그리고 verify 스킬 자체. 사용자가 요청하지 않는 한 실행 중 제품 코드를 절대 편집하지 마세요. 속성이 현재 코드에 실패하면 통과하도록 속성이나 모델을 약화시키지 마세요. 실패를 보고하세요.

## 패스

1. **검사를 찾으세요.** verify 스킬은 고정된 이름이 없으므로 그것이 하는 것으로 찾으세요: 명명된 코드에 대해 모델 체커, 증명기 또는 다른 검증기를 실행하는 프로젝트 스킬. 찾은 각각을 읽거나 사용자가 명명한 것을 읽으세요. 각 검사에 대해 속성, 커버하는 코드, 경계와 가정, 실행하는 명령, 그리고 코드를 설명한다고 마지막으로 확인된 커밋을 수집하세요. verify 스킬이 존재하지 않으면 멈추고 `/create-formal-verification-skill`을 가리키세요. 스킬이 동기화 커밋을 기록하지 않으면 검증 파일을 변경한 마지막 커밋을 사용하고 그렇게 했다고 말하세요.

2. **그대로 실행하세요.** 무언가를 변경하기 전에 각 검사를 한 번 실행하고 결과를 기록하세요. 여기서 통과는 코드가 올바르다는 것을 말하지 않습니다. 오래된 설명이 여전히 유지된다는 것을 말합니다. 여기서 실패는 드리프트 또는 버그일 수 있습니다. 5단계까지 어느 것인지 결정하지 마세요.

3. **커버된 코드의 모든 변경을 읽으세요.** 동기화 커밋에서 현재 커밋까지 커버된 파일을 diff하고, 각 커밋 메시지를 읽으세요. 이동한 코드도 찾으세요: 이름이 변경되거나 분할되거나 다른 파일로 이동된 커버된 함수는 여전히 커버된 코드입니다. 검사가 보호하는 상태를 터치하는 새 코드도 찾으세요. 동일한 필드를 작성하는 새 함수와 같은. 각 변경에 대해 다음 중 어느 것인지 결정하세요:
   - **효과 없음.** 변경이 검증이 설명하는 것을 변경하지 않습니다. 포맷팅, 주석 또는 검증이 커버하지 않는 코드 경로와 같은. 커밋 메시지가 아니라 모델 또는 하니스에 대해 이것을 확인하세요.
   - **검증이 더 이상 코드를 설명하지 않음.** 하나의 분할 불가능한 액션이었던 단계가 이제 둘이고, 분기가 추가되거나 제거되었고, 검사가 이동했고, 새 경로가 보호된 상태에 도달하거나, 값이 이제 다른 범위를 갖습니다. 모델 또는 하니스가 변경되어야 합니다.
   - **약속이 의도적으로 변경됨.** 변경이 코드가 약속하는 것을 변경하고, 변경의 증거가 이것이 의도된 것이라고 말합니다: 문서 주석, 테스트, 변경 로그 또는 커밋 메시지. 속성이 변경되어야 하며, 그 증거를 인용해야 합니다.
   - **약속이 깨질 수 있음.** 코드가 변경되었고, 약속이 변경되었다는 증거가 없습니다. 뒤따르는 실패를 버그 후보로 취급하세요.

4. **결과가 아니라 코드에서 업데이트하세요.** 모델 또는 하니스를 변경하여 변경된 각 부분이 리뷰어가 열 수 있는 코드를 다시 가리키도록 하고, 코드에서 하나의 분할 불가능한 단계를 검증에서 하나의 단계로 유지하세요. 다시 실행하기 전에 코드에서 업데이트를 작성하고, 검사를 통과하게 만드는 것으로 그것을 형성하지 마세요. 의도적으로 변경된 약속에 대해서만 속성을 변경하세요. 오래된 표현, 새로운 표현 및 증거를 작성하세요. 변경이 그것들을 틀리게 만들지 않는 한 경계를 유지하세요. 경계를 줄여야 하면 보고서에서 그렇게 말하세요.

5. **다시 실행하고 각 결과를 판단하세요.**
   - **Pass (통과):** 검사는 이제 실패 능력을 잃은 설명에 대해 통과할 수 있습니다. 속성이 보호하는 방식으로 새 코드를 깨뜨리세요. 새 검사를 제거하거나 새 단계를 재정렬하는 것과 같은. 검사가 그것을 잡는지 확인하세요. 그런 다음 중단을 삭제하세요.
   - **Fail (실패):** 실제 코드에 대해 단계별로 반례를 재생하세요. 단계가 코드에서 발생할 수 없으면 검증이 틀렸습니다. 검증을 수정하고, 무엇이 잘못되었는지 말하세요. 모든 단계가 발생할 수 있으면 버그입니다. 그것을 도입한 커밋을 명명하고, 반례를 코드 자체 단어로 단계 시퀀스로 말하고, 피해를 한 문장으로 진술하세요. 실제 코드에 대한 저렴한 테스트 또는 재현이 버그를 보여주면 증거로 보고서에 추가하세요. 제품 코드에 커밋하지 마세요.

6. **verify 스킬을 업데이트하세요.** 각 검사가 커버하는 코드, 명령, 경계, 가정 및 동기화 커밋을 업데이트하세요. 동기화 커밋을 확인한 커밋으로 설정하세요. 차단된 검사에 대해 동기화 커밋을 이동하지 말고 보고서에서 그렇게 말하세요. 그런 다음 다음 에이전트가 하듯이 verify 스킬을 한 번 따라서 그 단계가 여전히 실행되는지 알 수 있도록 하세요.

## 보고

사용자에게 각 검사에 대해 말하세요:

- 결과 및 읽은 커밋;
- 검증에서 변경된 것과 이유, 각 변경에 대한 짧은 이유와 함께: 코드가 형태를 변경했거나, 약속이 의도적으로 변경됨 (증거와 함께);
- 재실행 결과 및 업데이트된 검사가 여전히 실패할 수 있음을 보여주기 위해 사용한 중단;
- 각 버그, 평범한 단어로: 코드의 단어로 단계로서의 반례, 피해, 그리고 그것을 도입한 커밋;
- 검증이 여전히 커버하지 않는 것, 커버해야 하지만 하지 않는 새 코드를 포함하여.

어떤 실패가 검증의 드리프트였고 어떤 것이 코드의 버그였는지 명백하게 말하세요. 업데이트하기 전에 통과했고 후에 실패한 검사의 경우, 오래된 통과가 오래된 설명에 있었다고 말하세요.

검증 업데이트를 모든 제품 수정과 별도로 자체 변경에 넣으세요.