C++ 생태계에서 ‘안전성(Safety)‘과 ‘형식 검증(Formal Verification)‘은 언제나 계륵 같은 존재였습니다. 모두가 중요하다고 말하지만, 막상 Production 레벨에 도입하려 하면 “그거 할 시간에 기능 하나 더 만들지”라는 핀잔을 듣기 십상이죠. 그런데 최근 금융 데이터의 거인 Bloomberg가 꽤 흥미로운 도구를 공개했습니다. 이름하여 Crane. Rocq(구 Coq) 정리 증명기(Theorem Prover)에서 검증된 C++ 코드를 추출해 주는 도구입니다.

솔직히 처음 소식을 들었을 때는 “또 학계에서나 쓸 법한 장난감이 나왔나?” 싶었습니다. 하지만 Bloomberg가 만들었다는 점, 그리고 그들의 거대한 레거시 C++ 코드베이스에 통합하려는 목적이라는 점이 제 엔지니어로서의 호기심을 자극했습니다. 오늘은 이 Crane이 과연 실무에서 쓸만한 물건인지, 아니면 그저 이상적인 실험인지 깊게 파헤쳐 보겠습니다.

왜 하필 Rocq에서 C++인가?

보통 형식 검증을 한다고 하면 OCaml이나 Haskell 같은 함수형 언어로 코드를 추출하거나, 아예 Rust로 재작성하는 것을 떠올립니다. 하지만 Bloomberg 같은 조직에게 ‘재작성(Rewrite)‘은 불가능에 가깝습니다. 수십 년간 쌓인 C++ 라이브러리, 빌드 시스템, 배포 파이프라인을 하루아침에 바꿀 순 없으니까요.

Crane의 접근 방식은 매우 실용적입니다:

1. Rocq 에서 핵심 로직을 작성하고 수학적으로 증명한다.
2. Crane 을 통해 이를 ‘가독성 있고(readable)’, ‘현대적인(modern)’ C++ 코드로 변환한다.
3. 기존 C++ 프로젝트에 헤더 파일처럼 끼워 넣는다.

이론상으로는 완벽해 보입니다. 버그가 없음을 수학적으로 보장받으면서도, 기존 인프라를 그대로 쓸 수 있으니까요. 하지만 우리 같은 시니어 엔지니어들은 알죠. “Silver Bullet은 없다”는 것을요.

코드 레벨에서의 충격: 성능은 안녕하십니까?

Hacker News 스레드에서 가장 뜨거운 논쟁이 된 부분은 바로 ‘생성된 코드의 품질’입니다. 함수형 언어의 불변성(Immutability)과 재귀적 데이터 구조를 C++로 옮길 때 발생하는 오버헤드 때문입니다.

한 유저가 tests/basics/levenshtein/levenshtein.cpp에서 발견한 코드를 보시죠:

struct Ascii {
  std::shared_ptr<Bool0::bool0> _a0;
  std::shared_ptr<Bool0::bool0> _a1;
  std::shared_ptr<Bool0::bool0> _a2;
  std::shared_ptr<Bool0::bool0> _a3;
  std::shared_ptr<Bool0::bool0> _a4;
  std::shared_ptr<Bool0::bool0> _a5;
  std::shared_ptr<Bool0::bool0> _a6;
  std::shared_ptr<Bool0::bool0> _a7;
};

이 코드를 보고 경악하지 않는 C++ 개발자가 있을까요? 8비트 문자를 표현하기 위해 8개의 std::shared_ptr를 사용하고 있습니다. 이건 메모리 파편화(Fragmentation)와 캐시 미스(Cache Miss)의 종합 선물 세트입니다. 만약 제 팀원이 코드 리뷰에 이런 PR을 올렸다면 당장 반려했을 겁니다.

하지만 여기서 Trade-off 를 냉정하게 봐야 합니다. Crane의 목표는 ‘High Frequency Trading(HFT)’ 엔진을 만드는 게 아닙니다. 복잡한 파서(Parser), 프로토콜 상태 머신, 규제 준수 로직처럼 “속도보다 정확성이 100배 더 중요한” 모듈을 타겟으로 합니다. C++로 짜다가 댕글링 포인터나 버퍼 오버플로우로 터지는 것보다는, 좀 느리더라도 수학적으로 완벽한 코드가 나은 영역이 분명히 존재합니다.

실용주의적 검증: CompCert와는 다르다

학계의 엄격한 기준에서 보면 Crane은 다소 느슨합니다. 유명한 검증 컴파일러인 CompCert 는 소스 코드부터 어셈블리까지 전 과정을 수학적으로 증명합니다. 반면 Crane은 “Rocq에서 C++로의 변환 과정” 자체를 완전히 증명하지는 않습니다.

GitHub Wiki의 Design Principles에서도 이를 명시하고 있습니다:

Crane deliberately does not start from a fully verified compiler pipeline in the style of CompCert.

이것은 버그가 발생할 가능성을 열어두는 것이지만, 동시에 유연성 을 줍니다. 완벽한 증명 파이프라인을 구축하느라 몇 년을 허비하는 대신, 당장 돌아가는 결과물을 내놓고 점진적으로 개선하겠다는 전략입니다. 저는 이 부분이 매우 ‘엔지니어링적’이라고 느꼈습니다. 완벽함 때문에 좋음을 포기하지 않는 태도죠.

물론, NatIntStd.v에서 언급된 것처럼 Rocq의 무한한 자연수(nat)를 C++의 유한한 정수(int)로 매핑할 때 발생하는 오버플로우 문제는 개발자가 직접 신경 써야 합니다. 즉, 도구가 모든 책임을 져주진 않는다는 뜻입니다.

나의 생각: 틈새시장을 위한 강력한 무기

Crane을 보며 2018년쯤 우리 팀이 겪었던 문제가 떠올랐습니다. 금융 프로토콜 파서를 C++로 직접 구현하다가 수많은 엣지 케이스 버그로 고생했었죠. 그때 만약 Crane이 있었다면, 파서 로직만 Rocq로 작성해서 뽑아내고 나머지 네트워크 레이어는 기존 C++을 썼을 겁니다. 성능 손실은 미미했을 것이고, 안정성은 비약적으로 올라갔을 테니까요.

Hacker News의 반응 도 비슷합니다. “성능이 끔찍하다”는 비판과 “복잡한 로직을 C++로 직접 짜서 디버깅하는 지옥보단 낫다”는 옹호가 공존합니다. 저는 후자에 한 표를 던집니다. 현대 컴퓨팅 환경에서 CPU 사이클은 저렴하지만, 엔지니어의 디버깅 시간과 프로덕션 장애 비용은 비싸니까요.

결론 (Verdict)

Crane은 모든 C++ 프로젝트를 위한 도구가 아닙니다. 게임 엔진이나 실시간 렌더링 파이프라인에 이걸 쓴다면 미친 짓입니다. 하지만 금융, 보안, 항공우주 등 Critical한 비즈니스 로직을 다루는 C++ 팀 에게는 매우 매력적인 옵션이 생겼습니다.

• 장점: 기존 C++ 인프라와 호환되는 검증된 코드. 논리적 결함 원천 차단.
• 단점: 충격적인 메모리 구조와 오버헤드. 함수형 패러다임에 익숙지 않은 팀에게는 높은 진입 장벽.
• 총평: “성능을 제물로 바쳐 신뢰를 소환한다.” 레거시 C++ 시스템의 심장부를 수술해야 하는 CTO라면, 메스를 들기 전에 Crane을 한번 검토해 보십시오.