돈 존슨(Don Johnson)은 2026년 8월 16일 AI 지원 소프트웨어 팀이 구현을 시스템 이해보다 빠르게 생성하면서 숨은 가정을 배포하고 있다고 주장했다. 생산 환경의 엣지 케이스는 린팅과 얕은 테스트를 통과할 수 있는데, QA가 경계, 상태 전이, 실패 모드, 불변조건(항상 참이어야 하는 조건)에 대한 공유 모델이 아니라 코드만 받기 때문이라고 설명했다.

제안된 신뢰성 스택은 C4에서 시작한다. C4는 소프트웨어를 컨텍스트, 컨테이너, 컴포넌트, 코드 수준에서 매핑하는 모델이다. Johnson은 모든 프로젝트에 4개 다이어그램이 필요한 것은 아니며, 많은 팀에는 컨텍스트와 컨테이너 다이어그램만으로 충분할 수 있다고 말했다. C4의 역할은 개발자나 QA가 저장소에서 추론하기 전에 사용자, 인접 시스템, 애플리케이션, 데이터 저장소, 서비스, 컴포넌트, 관계, 소유권, API, 신뢰 경계를 보이게 하는 것이다.

두 번째 계층은 TLA+다. 레슬리 램포트(Leslie Lamport)는 TLA+를 코드보다 높은 수준에서 정밀한 모델을 작성하는 언어, 특히 동시성·분산 시스템에 적합한 언어로 설명한다. Johnson은 TLA+와 TLC 모델 체커가 동작을 탐색하고 명시된 속성을 위반하는 추적을 찾을 수 있다고 말했다. AI는 첫 명세 초안을 만들고, 자연어 약속을 후보 불변조건으로 바꾸며, 반례 추적을 설명하고, 모델 개선을 도울 수 있다. 다만 어떤 약속이 올바른지는 사람이 결정해야 한다.

세 번째 계층은 결정적 시뮬레이션 테스트(DST)다. DST는 시간, 무작위성, 스케줄링, 네트워크, 저장소, 장애를 조작할 수 있는 통제된 세계에서 실제 구현 코드를 실행한다. Johnson은 TigerBeetle의 VOPR를 예로 들며, 단일 스레드에서 클러스터를 시뮬레이션하고 시간을 가속하며 저장소 장애를 주입할 수 있다고 설명했다. 모델 체킹은 알고리즘 오류를 드러낼 수 있고, 시뮬레이션은 특정 구현과 그 가정을 실행해 본다는 차이가 있다.

Johnson은 AI 생성 코드가 풍부한 환경을 위한 6단계 워크플로를 제시했다. 자연어로 약속을 명시하고, C4로 경계를 그리며, TLA+로 위험한 동작을 모델링하고, 검토된 의도에서 구현을 생성한 뒤, 구현을 결정적으로 공격하고, 운영 관찰이나 시뮬레이션 실패를 다시 모델에 반영하는 방식이다. 가벼운 버전은 컨텍스트 다이어그램 1개, 컨테이너 다이어그램 1개, 작성된 불변조건 5개, 가장 위험한 전이를 위한 작은 모델, 시드가 있는 테스트 하니스가 될 수 있다고 했다.

Johnson은 할머니가 AI로 만든 가족 사진 앨범을 비금융 분야의 미션 크리티컬 약속 사례로 들었다. 원본 사진은 절대 파괴돼서는 안 되고, 비공개 사진은 실수로 노출돼서는 안 되며, 캡션과 연대기는 모든 편집 뒤에도 유지돼야 하고, 가족 구성원 2명이 서로의 변경사항을 덮어써서는 안 된다. Johnson은 AI가 코드를 만들 수는 있지만, 시스템의 목적을 정하고 약속을 보이게 만들며 그 약속이 깨졌을 때 책임을 받아들이는 일은 여전히 인간에게 남아 있다고 결론냈다.

돈 존슨(Don Johnson)은 2026년 8월 16일 AI 지원 소프트웨어 팀이 구현을 시스템 이해보다 빠르게 생성하면서 숨은 가정을 배포하고 있다고 주장했다. 생산 환경의 엣지 케이스는 린팅과 얕은 테스트를 통과할 수 있는데, QA가 경계, 상태 전이, 실패 모드, 불변조건(항상 참이어야 하는 조건)에 대한 공유 모델이 아니라 코드만 받기 때문이라고 설명했다.

제안된 신뢰성 스택은 C4에서 시작한다. C4는 소프트웨어를 컨텍스트, 컨테이너, 컴포넌트, 코드 수준에서 매핑하는 모델이다. Johnson은 모든 프로젝트에 4개 다이어그램이 필요한 것은 아니며, 많은 팀에는 컨텍스트와 컨테이너 다이어그램만으로 충분할 수 있다고 말했다. C4의 역할은 개발자나 QA가 저장소에서 추론하기 전에 사용자, 인접 시스템, 애플리케이션, 데이터 저장소, 서비스, 컴포넌트, 관계, 소유권, API, 신뢰 경계를 보이게 하는 것이다.

두 번째 계층은 TLA+다. 레슬리 램포트(Leslie Lamport)는 TLA+를 코드보다 높은 수준에서 정밀한 모델을 작성하는 언어, 특히 동시성·분산 시스템에 적합한 언어로 설명한다. Johnson은 TLA+와 TLC 모델 체커가 동작을 탐색하고 명시된 속성을 위반하는 추적을 찾을 수 있다고 말했다. AI는 첫 명세 초안을 만들고, 자연어 약속을 후보 불변조건으로 바꾸며, 반례 추적을 설명하고, 모델 개선을 도울 수 있다. 다만 어떤 약속이 올바른지는 사람이 결정해야 한다.

세 번째 계층은 결정적 시뮬레이션 테스트(DST)다. DST는 시간, 무작위성, 스케줄링, 네트워크, 저장소, 장애를 조작할 수 있는 통제된 세계에서 실제 구현 코드를 실행한다. Johnson은 TigerBeetle의 VOPR를 예로 들며, 단일 스레드에서 클러스터를 시뮬레이션하고 시간을 가속하며 저장소 장애를 주입할 수 있다고 설명했다. 모델 체킹은 알고리즘 오류를 드러낼 수 있고, 시뮬레이션은 특정 구현과 그 가정을 실행해 본다는 차이가 있다.

Johnson은 AI 생성 코드가 풍부한 환경을 위한 6단계 워크플로를 제시했다. 자연어로 약속을 명시하고, C4로 경계를 그리며, TLA+로 위험한 동작을 모델링하고, 검토된 의도에서 구현을 생성한 뒤, 구현을 결정적으로 공격하고, 운영 관찰이나 시뮬레이션 실패를 다시 모델에 반영하는 방식이다. 가벼운 버전은 컨텍스트 다이어그램 1개, 컨테이너 다이어그램 1개, 작성된 불변조건 5개, 가장 위험한 전이를 위한 작은 모델, 시드가 있는 테스트 하니스가 될 수 있다고 했다.

Johnson은 할머니가 AI로 만든 가족 사진 앨범을 비금융 분야의 미션 크리티컬 약속 사례로 들었다. 원본 사진은 절대 파괴돼서는 안 되고, 비공개 사진은 실수로 노출돼서는 안 되며, 캡션과 연대기는 모든 편집 뒤에도 유지돼야 하고, 가족 구성원 2명이 서로의 변경사항을 덮어써서는 안 된다. Johnson은 AI가 코드를 만들 수는 있지만, 시스템의 목적을 정하고 약속을 보이게 만들며 그 약속이 깨졌을 때 책임을 받아들이는 일은 여전히 인간에게 남아 있다고 결론냈다.