---
title: "Dafny: 검증 기반 프로그래밍 언어"
published: 2025-12-16T22:50:59.000Z
canonical: https://jeff.news/article/931
---
# Dafny: 검증 기반 프로그래밍 언어

Microsoft가 개발한 검증 기반 프로그래밍 언어로, 코드에 명세를 기록하면 정적 검증기가 자동으로 정확성을 증명함. C#, Java, JavaScript, Go, Python으로 컴파일 가능하며 IDE 플러그인 등 개발 생태계를 갖추고 있음.

- Microsoft가 개발한 검증 기반(verification-aware) 프로그래밍 언어로, 명세(specification)를 코드에 직접 기록하고 정적 검증기가 구현이 명세에 부합하는지 자동으로 증명해줌
- C#, Java, JavaScript, Go, Python으로 컴파일이 가능해 기존 개발 워크플로우에 바로 통합할 수 있으며, 추가 타겟 언어도 계획 중임
- 수학적 정수/실수, 비트벡터, 클래스, 제네릭 타입, 귀납적 데이터 타입, 람다 표현식, 패턴 매칭 등 일반적인 프로그래밍 개념을 폭넓게 지원함
- IDE 플러그인, LSP 기반 언어 서버, 코드 포매터, 레퍼런스 매뉴얼, 튜토리얼 등 개발 생태계가 갖춰져 있음
- 테스트만으로는 놓칠 수 있는 후반부 버그를 개발 단계에서 수학적으로 검증해 제거하는 것이 핵심 목표임

## 핵심 포인트

- 명세를 코드에 직접 기록하고 정적 검증기가 구현의 정확성을 자동 증명
- C#, Java, JavaScript, Go, Python 등 5개 언어로 컴파일 가능
- IDE 플러그인, LSP 언어 서버, 코드 포매터 등 개발 생태계 구비
- 테스트로 놓칠 수 있는 버그를 개발 단계에서 수학적으로 제거하는 것이 목표

## 인사이트

테스트 기반 검증의 한계를 수학적 증명으로 보완하려는 접근으로, 고신뢰성이 요구되는 시스템 개발에서 주목할 만한 도구임.