우리는 언어 모델(Language Models)에 의해 생성되도록 의도된 하드웨어 기술 언어(Hardware Description Language, HDL)인 ARCH를 위한 최초의 일급 IEEE-754 binary32 (FP32) 및 bfloat16 (BF16) 산술 연산의 설계 및 엔드 투 엔드(end-to-end) 검증 결과를 보고합니다. 비교(comparisons), 변환(conversions), 덧셈(add), 뺄셈(sub), 곱셈(mul), 그리고 융합 곱셈-덧셈(Fused Multiply-Add, FMA)을 포함한 모든 연산자는 단일 비트 벡터 IR(Intermediate Representation)을 대상으로 한 번 기술되며, 하나의 소스로부터 세 가지 방식인 합성 가능한 SystemVerilog, SMT-LIB 모델, 그리고 Lean 4 증명 모델로 렌더링됩니다. 이 세 가지 산출물은 구조적으로 서로 어긋날 수 없으며, 잔여 노드별 프린터 대응 관계는 기계적으로 확인됩니다. Yosys-to-SMT 미터(miter)를 통해 생성된 SystemVerilog가 24개 모든 연산자에 대해 SMT 모델과 동일함을 증명합니다. 검증은 솔버 처리 가능성(solver-tractability)의 경계에서 나뉩니다. 곱셈기가 없는 연산자(비교, 모든 2^64 입력에 대한 add/sub, 변환, 그리고 모든 binary BF16 산술)는 SMT-LIB FloatingPoint 이론과 완전히 동일함이 전수 증명되었습니다. SAT-hard 문제인 곱셈기를 포함하는 연산자(FP32 mul 및 FMA)는 Lean에서 정확한 dyadic 값에 대한 값 수준의 round-to-nearest-even 명세에 대해 오류가 없음을(sorry-free) 올바르게 반올림됨이 증명되었습니다. 물리적 특성 분석 결과 FMA가 타이밍 아웃라이어로 나타났습니다. FMA의 정확한 광폭(exact-wide) 470비트 데이터패스는 우리의 흐름에서 파이프라이닝되지 않습니다. 우리는 이를 Nangate45에서 268 MHz로 파이프라이닝되는 제한된 98비트 guard/round/sticky 데이터패스로 재구현하였으며, Lean을 통해 모든 2^96 입력에 대해 이것이 정확한 광폭 참조 모델과 비트 단위로 동일함을 증명하여 참조 모델의 검증된 정확한 반올림 특성을 상속받도록 했습니다. 이 동등성은 공유된 곱셈기가 양쪽 모두에 나타나 상쇄되기 때문에 처리가 가능합니다. 즉, SAT 솔버나 증명 과정에서 곱셈기 동등성을 해결할 필요가 없습니다. (BF16 FMA는 의도적으로 FP32-accumulating fusion으로 설계되었으며, 정확히 그렇게 정의됩니다.) 모든 기계 확인된 주장(machine-checked claims)은 태그가 지정된 오픈 소스 릴리스에 고정되어 있습니다.