Ilia Zaichuk

Software engineer focused on formal verification, verified compilation, and high-assurance systems.

resume · email · github · linkedin

Publications

• HELIX: Verified compilation of cyber-physical control systems to LLVM IR

  Preprint, 2026. Manuscript under review.

  A verified compiler pipeline that lowers mathematical descriptions of numerical control code to LLVM IR while checking transformations in Rocq.

• Modular, compositional, and executable formal semantics for LLVM IR

  ICFP'21

  A compositional Rocq semantics for LLVM IR built around interaction trees, with an executable interpreter.

• Verified Translation Between Purely Functional and Imperative Domain Specific Languages in HELIX

  VSTTE'20

  A focused account of HELIX's translation from functional operator languages to imperative languages with memory and floating-point computation.

• Formal verification of floating-point number conversion between ASN.1 BER and IEEE 754 binary encodings

  POPL'19 SRC, undergraduate category third place

  A Rocq development for verifying conversion between ASN.1 BER encodings and IEEE 754 floating-point representations.

Projects

• Theseus

  A small Go file server organized around stable URLs and backend-independent storage.

• LEG-16

  A 16-bit CPU built in Turing Complete from NAND-level components, with assembly tooling and compact circuit designs.

• float-cohorts

  A Rocq library for reasoning about floating-point representations through exact cohorts rather than machine formats directly.