F*: 범용 증명 지향 프로그래밍 언어

개요

F*는 의존적 타입, SMT 해결기, 전술 기반 대화형 정리를 통해 순수 함수형 및 효과형 프로그래밍을 모두 지원하는 범용 증명 지향 프로그래밍 언어입니다.

이 언어는 F로 구현되었으며 OCaml을 사용하여 부트스트랩됩니다. 핵심 설계는 풍부한 사양을 표현하기 위해 의존적 타입에 의존하며, 증명 자동화는 SMT 해결기와 대화형 전술 언어를 통해 제공됩니다. F 프로그램은 함수형 스타일로 작성하거나 상태, 예외, 동시성과 같은 효과를 사용하여 작성할 수 있으며, 동일한 언어를 사용하여 프로그램과 그 정확성 증명을 모두 작성합니다.

컴파일 대상

기본적으로 F* 프로그램은 OCaml로 컴파일되며, 추가로 F#, C, WebAssembly, KaRaMeL 및 Vale를 통한 검증된 어셈블리로의 추출 경로가 있습니다.

기본적으로 F* 컴파일러는 OCaml 런타임과 연결할 수 있는 OCaml 코드를 내보냅니다. KaRaMeL 도구는 F의 부분집합(저수준 포함 Low)을 C 또는 WebAssembly로 추출합니다. Vale 툴체인은 저수준 F* 조각을 어셈블리 언어로 추출하여 성능‑중요한 코드의 검증을 가능하게 합니다. 이러한 추출 메커니즘은 동일한 소스를 여러 백엔드로 대상으로 삼으면서 기능적 정확성 보존을 유지할 수 있게 합니다.

설치 및 배포

F*는 Apache 2.0 라이선스로 출시되며, GitHub 릴리스에서 Windows, Linux, macOS용 바이너리를 제공하며, OPAM, Docker, Nix 및 소스 빌드도 제공합니다.

사용자는 GitHub의 F* 릴리스 페이지에서 사전 빌드된 바이너리를 다운로드할 수 있습니다. 대체 설치 방법으로는 OPAM 패키지, Docker 이미지, Nix 표현식, 또는 INSTALL.md에 있는 지침을 따라 소스에서 빌드하는 것이 있습니다. 모든 배포 채널은 Microsoft Research, Inria 및 커뮤니티의 F* 개발 팀에서 유지 관리됩니다.

학습 자료

F의 주요 학습 자료는 "Proof-oriented Programming In F"이라는 제목의 온라인 책이며,これに加えて Low* 튜토리얼과 계절 학교에서 제공되는 다양한 강의 자료가 있습니다.

책 "Proof-oriented Programming In F*"은 정기적으로 업데이트되며 F* 웹사이트에서 PDF로 제공됩니다. accompanying 튜토리얼 페이지는 브라우저에서 시도할 수 있는 스냅샷과 연습 문제를 제공합니다. 별도의 튜토리얼은 KaRaMeL을 통해 C로 컴파일되는 F의 저수준 부분인 Low를 다룹니다. Oregon Programming Language Summer School(2019, 2021), ECI 2019, EUTypes Summer School 2018과 같은 행사의 강의 자료도 온라인으로 출판되어 강의 노트, 슬라이드, 코드 예제를 포함합니다.

Low* 부분집합

Low는 KaRaMeL을 통해 C로 컴파일할 수 있는 F의 저수준 부분집합으로, 검증된 시스템 프로그래밍을 가능하게 합니다.

Low는 메모리 레이아웃을 직접 제어하고 인라인 어셈블리를 유지하면서 의존적 타입 시스템을 유지하는 시스템 코드에 적합한 조각으로 F를 제한합니다. Low로 작성된 코드는 F에서 정확성을 입증한 후 효율적인 C로 추출할 수 있어 검증된 암호화 프리미티브, 파서 및 OS 구성 요소 개발에 적합합니다.

커뮤니티 및 지원

F* 커뮤니티는 GitHub Discussions, 공개 Zulip 포럼, 저트래픽 메일링リスト, 월간 PoP Up 세미나를 통해 소통 및 지원을 합니다.

질문과 발표는 GitHub Discussions 포럼에서 처리됩니다. 공개 Zulip 채팅(fstar.zulipchat.com)은 주요 실시간 토론 장소로 사용됩니다. Google Groups 메일링リスト는 저트래픽 발표를 위해 존재합니다. F* PoP Up 세미나는 사용자 및 개발자 회의로 불규칙하게 개최되지만 월간 주기를 목표로 합니다. 유지 관리자는 fstar-maintainers@googlegroups.com으로 연락할 수 있습니다.

산업 및 학술 활용

F*는 여러 고보증 프로젝트에서 사용되며, 가장 주목할 만한 것은 Firefox, Linux 커널, Python, mbedTLS, Tezos, ElectionGuard, Wireguard, Windows Hyper‑V 및 ebpf‑for‑windows에 배포된 검증된 암호화 라이브러리와 파서를 생성하는 Project Everest입니다.

Project Everest는 검증된 암호화 라이브러리인 HACL*, 검증된 어셈블리 암호화인 ValeCrypt, 그리고 결합된 제공자인 EverCrypt를 개발합니다. EverParse는 바이너리 형식에 대한 검증된 파서를 생성합니다. 이러한 아티팩트는 프로덕션 소프트웨어에 통합되었습니다: Firefox는 TLS에 HACL를 사용하고, Linux 커널은 HACL curve25519 코드를 포함하며, Python의 암호화 라이브러리는 HACL를 포함하고, mbedTLS는 EverCrypt를 번들로 제공하며, Tezos는 HACL로 전환했으며, ElectionGuard는 EverCrypt에 의존하고, Wireguard는 암호화 작업에 HACL*를 사용하며, Windows Hyper‑V는 EverParse‑생성된 파서를 네트워크 패킷에 사용하고, ebpf‑for‑windows 프로젝트는 eBPF 프로그램 로딩에 EverParse를 사용합니다.

연구 기초

F*에 대한 연구는 언어 설계, 의미론 및 효과, 보안 및 암호화, 시스템, 파싱, 프로그래밍 및 프로그램 분석, AI‑지원 프로그래밍을 포괄하며, 프로젝트 참고문헌에 인용된 수많은 동료 검토 논문이 있습니다.

주요 작품으로는 핵심 언어를 설명하는 POPL 2016 논문 "Dependent Types and Multi-monadic Effects in F*", Low를 소개하는 ICFP 2017 논문 "Verified Low-level Programming Embedded in F", Vale를 제시하는 POPL 2019 논문 "A Verified, Efficient Embedding of a Verifiable Assembly Language", 그리고 SMT, 전술 및 메타프로그램을 통한 증명 자동화를 설명하는 ESOP 2019 논문 "Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms"가 있습니다. 추가 논문으로는 Dijkstra 모나드, Steel 및 SteelCore 동시 분리 로직, USSL 및 PulseCore, 그리고 암호화, 시스템, 파싱 및 프로그래밍 언어 구현에서의 다양한 애플리케이션‑특정 검증이 있습니다.

보안 및 암호화에서의 응용

F*는 TLS 1.3, QUIC, Signal, post‑quantum TLS 및 다양한 인증된 암호화 구성을 포함한 암호화 프로토콜과 구현을 검증하는 데 적용되었습니다.

주요 검증된 아티팩트로는 TLS‑1.3 레코드 레이어(S&P 2017), HACL*(CCS 2017), EverCrypt(S&P 2020), HACL×N(CCS 2020), QUIC 레코드 레이어(S&P 2021), DICE 측정된 부트(USENIX Security 2021), 상징적 프로토콜 분석을 위한 DY* 프레임워크(Euro S&P 2021), 보안 채널 프로토콜을 위한 Noise* 라이브러리(S&P 2022), MLS를 위한 TreeSync(USENIX Security 2023), 그리고 프로토콜‑인식 파싱을 위한 Comparse(CCS 2023)가 있습니다. 최근 작업에서는 F*로 번역하여 Rust TLS‑1.3 구현을 검증하기도 했습니다(CCS 2025).

시스템에서의 응용

F*는 메모리 할당자, 샌드박싱, 데이터 무결성 모니터, 동시 키‑값 저장소 검증에 사용됩니다.

예시로는 검증 가능한‑안전한 WebAssembly 샌드박스(USENIX 2022), 데이터 무결성 모니터링을 위한 FastVer 및 FastVer2(SIGMOD 2021, CPP 2022), 반응형 실시간 시스템을 위한 Pipit(ECOOP 2024), 그리고 Steel에서 검증된 강화된 동시 메모리 할당자인 StarMalloc(SPLASH 2024)이 있습니다.

파싱에서의 응용

F는 EverParse 및 ASN1과 같은 검증된 파서 생성기를 이끌며, CBOR, CDDL, COSE 및 ASN.1 DER과 같은 바이너리 형식에 대한 검증된 C 파서를 생성합니다.

EverParse는 USENIX Security 2019에서 소개되었으며 나중에 Hyper‑V 패킷 파서를 강화하는 데 사용되었습니다(PLDI 2022). ASN1은 검증된 ASN.1 DER 파싱을 제공합니다(CPP 2022). 최근 작업에서는 F에서 CBOR, CDDL 및 COSE를 형식화하고 Pulse(CCS 2025)를 통해 검증된 파서와 포매터를 개발했습니다.

프로그래밍, 프로그램 증명 및 프로그램 분석에서의 응용

F*는 가역 회로의 검증된 컴파일, 세션‑타입 멀티파티 프로토콜, 추상 해석기, 법률을 위한 도메인 특수 언어, 그리고 Rust 및 OCaml 코드의 검증을 지원합니다.

주요 결과로는 가역 회로를 위한 검증된 컴파일러(CAV 2018), 멀티파티 프로토콜을 위한 Session*(OOPSLA 2020), F에서 검증된 추상 해석 프레임워크(SAS 2021), 검증된 컴파일러 부분을 갖춘 법률 언어 Catala(ICFP 2021), Merkle Patricia 트리 검증(arXiv 2021), 기능 정확성을 위해 Rust를 F로 번역하는 Aeneas(ICFP 2022), 양자 분리 논리를 위한 SteelCore 적응 Q*(PlanQC 2022), 검증되지 않은 코드와의 안전한 상호작용을 위한 SecIO* 및 SecRef*(POPL 2024, ICFP 2025), 그리고 F* 및 Low*에서 검증된 OCaml용 기계적으로 검증된 가비지 컬렉터(JAR 2025)가 있습니다.

AI‑지원 프로그래밍 노력

최근 작업에서는 신경 합성과 AI 에이전트를 탐색하여 F* 프로그램과 증명 생성을 자동화하고, 자연 언어에서 바이너리 형식 사양을 도출합니다.

ICSE 2025 논문 "Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming"은 프로그램과 증명 합성을 위한 모델을 훈련하기 위한 큰 F* 코드 코퍼스를 큐레이션합니다. arXiv 논문 "3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers"는 RFC와 예시를 형식 사양으로 변환하여 EverParse와 함께 사용할 수 있는 에이전트를 개발합니다.

Hacker News에서의 커뮤니티 피드백

Hacker News 게시물의 댓글에서는 더 눈에 띄는 구문 예시를 원했고, 산업 채택에 대해 문의했으며, 컴파일러 검증과 저수준 프로그래밍에 대한 언어의 적합성을 논의했습니다.

"Clicked like 5 pages and never found 1 code example. Idk why languages don't have their syntax in a sandbox front-and-center on the home page. It's like a video game site with zero screenshots or videos (also rampant). New programming languages I want 2 things: 1. What does the syntax look like 2. Why would I use this language Talk about the proof logic, show the syntax, thank you" – @cyanregiment

"I liked being able to express calling external libraries while incrementally migrating existing C codebases to F*. Very solid language." – @pvsnp

"https://fstar-lang.org/tutorial/" – @LelouBil

"I like Haskell, and to me this seems really useful as a kind of "noob" to functional languages. Is this used in the industry ? And for what kind of software ?" – @LelouBil

"Guess responsive stylesheets can't be implemented without side effects..." – @boutell

"Would this language be useful for implementing compilers and formally proving things about them?" – @3lambda

"Looks very very interesting and exciting! Key question: is anyone using it anger and has experience to share?" – @_doctor_love

"F* seems to be a collection of like five different languages and proof systems. Honestly I never figured it out. Does it get basic stuff like subtraction and u8 right, unlike Lean?" – @IshKebab

"- stupid question: why dont we have a programming language that looks like typed python but runs much faster than c++, zig and rust" – @vivzkestrel