안무 프로그래밍(Choreographic programming, CP)은 동시적이고 분산된 시스템을 올바르게 구축하는 개발 패러다임입니다. 프로그래머는 전역적인 관점에서 시스템의 의도된 전체 동작을 안무(choreography) 형태로 작성하고, 이 안무는 엔드포인트 투영(endpoint projection, EPP)이라는 절차를 통해 통신하는 엔드포인트 프로그램으로 자동 컴파일됩니다. 핵심 약속은 이렇게 투영된 엔드포인트 프로그램들이 함께 실행될 때, 원본 안무와 동작적으로 동등하다는 것입니다. 이 약속을 충족시키는 것은 표현력이 풍부한 CP 언어에 있어 까다로운 문제가 됩니다. 기존의 CP 기계화(mechanisation)들은 제한적인 조각만을 다루며, 풍부한 기능을 가진 교과서적이고 일반 목적의 언어 구현체들은 중요한 상호작용들을 비형식적으로 남겨둡니다. 특히, 선택 지식에서의 일반 분기(general branching in knowledge of choice), 일반 재귀(general recursion), 그리고 안무에서의 비결정론적 선택(nondeterministic choice)은 아직 기계 검증 이론에 통합되지 않았습니다. 우리는 이러한 특징들을 포착하는 CP의 새로운 기계화인 Mech를 Lean 4로 제시합니다. Mech 개발에는 두 가지 중심적인 기술적 과제가 있었습니다. 첫째, 문헌에서 스케치된 의미론(semantics)이 비결정론적 선택이 동시성(concurrency)과 어떻게 상호작용하는지를 정확하게 포착하지 못한다는 점입니다. 따라서 우리는 비결정론적 안무 실행을 투영된 엔드포인트 프로그램의 동작과 일치시키는 새로운 의미론을 공식화했습니다. 둘째, 이러한 모든 특징들을 증명에서 관리하는 것이 복잡하다는 점입니다. 우리는 이를 해결하기 위해 안무 자체, 그 의미론에 사용되는 연산자들, EPP, 그리고 이들의 조합에 대한 새로운 대수학적 법칙(algebraic laws)을 밝혀냈습니다. 우리의 개발을 사용하여, 우리는 EPP의 완전성(completeness)과 건전성(soundness)을 증명하고, 투영된 네트워크에 대해 통신 안전성(communication safety)과 교착 상태 자유성(deadlock-freedom)을 도출함으로써, 현재까지 가장 광범위한 CP 기계화 이론을 제시합니다.