# specdown > 마크다운 + 명세서. 마크다운 문서 안에 인수 테스트를 적어서 실행 가능한 소프트웨어 명세서를 작성하는 방식이다. 에이전틱 엔지니어링 실험 4의 결과물. [마크다운](https://wiki.g15e.com/pages/Markdown.txt) + 명세서. 마크다운 문서 안에 <인수 테스트>를 적어서 실행 가능한 소프트웨어 명세서를 작성하는 방식이다. [에이전틱 엔지니어링 실험 4](https://wiki.g15e.com/pages/Agentic%20engineering%20experiment%204.txt)의 결과물. - https://corca-ai.github.io/specdown (홈페이지이자 명세서) - https://github.com/corca-ai/specdown (소스코드) ## 부연 자연어 문서의 단점: - 자연어 문서와 코드 사이에 불일치가 생겼을 때 찾아내기가 어렵다. 내 경우엔 코드가 대충 40,000줄(주석 및 빈줄 제외) 정도 되는 시점에 코딩 에이전트들이 실수를 하기 시작했다. (2025년 3월 기준) - 생각한 걸 자연어로 정확히 표현하기는 어렵다. 설사 정확히 표현했다고 하더라도 그에 따른 귀결이 예상과는 다른 경우가 많다. (참고: [자연어로 작성된 명세서](https://wiki.g15e.com/pages/Specification%20written%20in%20natural%20language.txt)) 전통적 테스트(E2E, Unit Tests)의 단점: - 모든 경우의 수를 테스트하는 게 현실적으로 불가능하다. - 필요한 테스트 케이스를 잘 발견하기가 쉽지 않다. 형식 모델 검증의 단점: - 읽고 쓰기가 어렵다. 이 셋을 엮으면 강력한 조합이 된다([Design is beneficially relating elements](https://wiki.g15e.com/pages/Design%20is%20beneficially%20relating%20elements.txt)). 자연어는 읽기 쉽고, Alloy 모델은 제한된 범위 내에서 모든 가능한 조합을 검증하고, 전통적인 테스트는 명세와 코드 사이를 결정론적으로 연결해준다. Alloy 모델의 사례(run)와 반례(check)는 좋은 테스트 케이스 후보를 알려주며, 주어진 설계에 의해 필연적으로 수반되는 속성들을 기계적으로 발견할 수 있기 때문에 불필요한 코드를 줄여준다. 자연어 명세와 모델과 전통적 테스트가 한 파일 안에 엮여 있으면, 모델과 문서와 코드 사이의 불일치 가능성을 대폭 줄일 수 있고 따라서 코딩 에이전트 및 인간의 실수를 줄일 수 있다. ## 실행 결과 화면 예시 마크다운 문서에서 frontmatter를 분리하는 기능에 대한 명세서의 일부. ![Pasted image 20260315150735.png](Pasted%20image%2020260315150735.png) ## See also - [Framework for integrated test](https://wiki.g15e.com/pages/Framework%20for%20integrated%20test.txt) - - [Alloy Analyzer](https://wiki.g15e.com/pages/Alloy%20Analyzer.txt)