CktFormalizer: Autoformalization of Natural Language into Circuit Representations
CKTFORMALIZER uses an LLM to generate hardware designs from natural language specifications, but it embeds these designs within Lean's dependently-typed system. This system acts as a type checker and correctness firewall, ensuring that generated code is structurally sound—free of errors like width mismatches or combinational loops—before any synthesis begins. It transforms the LLM's generation loop into a type-guided refinement process for high backend realizability.