Hardware and Firmware Formal Methods Engineer

Sigil Logic builds AI for rigorous engineering. Our platform, HOARDE, is a multi-agent system that brings formal methods and model-based engineering into the workflows teams already use. It connects requirements, architecture, software, firmware, hardware, tests, and proofs; orchestrates the right verification tools for each problem; and produces an auditable record of why a system works.

We are building for teams whose systems must not fail. Our mission is to make high-assurance engineering practical and scalable: to turn decades of research and experience on nationally critical systems into an everyday engineering capability.

We believe formal methods are among the most powerful ways to make AI-generated systems trustworthy. We are working at the frontier where LLMs, automated reasoning, and real hardware and software meet—and we believe that combination will reshape how engineering is done.

We are expanding HOARDE's hardware and firmware capabilities in response to customer demand. We are looking for an engineer who can reason across the boundary between architecture, RTL, and low-level software—and help make rigorous verification part of how those systems are built.

Your work will have two closely connected parts. You will extend HOARDE and its verification toolchain, then use those capabilities on real hardware and firmware. Early work may emphasize tool integration and formal models; as those capabilities mature, more of your time will move toward applying them to production artifacts and delivering verified results.

The problems span processor and accelerator architectures, RISC-V and instruction-set models, Verilog and SystemVerilog RTL, and firmware and drivers written in C or Rust. Depending on your background, you might arrive as a hardware engineer who practices formal verification, a formal-methods engineer comfortable with hardware, or a firmware verification engineer ready to work across the full boundary.

• Specify and verify hardware and firmware behavior, from architectural and instruction-set models through RTL, drivers, and low-level code.
• Develop properties, invariants, reference models, and proof strategies; run model checking, symbolic execution, equivalence checking, and solver-backed verification; and turn counterexamples into diagnoses and fixes.
• Build deep capability in Yosys-based formal hardware verification and related flows, improving the tools and integrations that make those workflows dependable and repeatable.
• Connect formal models—such as Sail models of instruction-set behavior—to Verilog/SystemVerilog implementations and the firmware that drives them.
• Integrate formal tools into HOARDE so that AI agents and human engineers can invoke them, understand their results, and act on the evidence they produce.
• Maintain traceability across requirements, architecture, design decisions, implementation, tests, and proofs, so that a change in one artifact is visible everywhere it matters.
• Work closely with hardware designers, firmware engineers, formal-methods specialists, and customers to decide where full proof is warranted and where lighter-weight assurance is the better engineering choice.
• Turn formal-methods work into durable product capabilities and verified results that customers can use.

• Hands-on experience with formal verification or automated reasoning. You understand concepts such as SAT/SMT solving, symbolic execution, model checking, theorem proving, higher-order logic, or property-based verification well enough to learn new tools quickly and use them with judgment.
• Practical engineering depth in hardware, firmware, or both. You can work directly with RTL such as Verilog/SystemVerilog, low-level C or Rust, or comparable implementation artifacts, and you are motivated to grow across the hardware/firmware boundary.
• A record of shipping usable tools, production systems, or verified technical outcomes.
• The ability to translate a real engineering question into the right specification, property, or assurance argument, and to explain the result clearly to people who are not formal-methods specialists.
• Strong engineering fundamentals, careful technical judgment, and the self-direction to make progress in a small, fully distributed team.
• Curiosity about AI-assisted and agentic engineering, and a desire to make generated hardware and software demonstrably trustworthy.

This role touches many tools and domains. Depth in any subset can be valuable.

• Yosys, SBY/SymbiYosys, Tabby CAD, or commercial formal hardware verification tools
• Verilog, SystemVerilog, SystemVerilog Assertions, Verilator, FPGA or ASIC toolchains, or hardware design and validation
• Sail, RISC-V, ISA modeling, processor or accelerator design, matrix extensions, dataflow architectures, or tensor-processing hardware
• C or Rust firmware and drivers; Cryptol and SAW; Frama-C, CBMC, Verus, Kani, or similar verification tools
• Rocq, Isabelle/HOL, or another interactive theorem prover
• Compartmentalized architectures such as CHERI, operating systems or hypervisors, compilers, or hardware/software interface verification
• Building formal-methods tools or integrating them into developer workflows, CI, and review systems

If the work sounds like you and you bring strong foundations in formal methods and hardware or firmware, relevant applied work, and the ability to learn, we want to hear from you.

Sigil Logic is a small, early team. You will work directly with people who have spent their careers building high-assurance systems, and you will have real influence over our product, methodology, and engineering culture. We value intellectual range, precise communication, practical output, and colleagues who teach what they know while learning from others.

We are headquartered in Portland, Oregon, and work as a fully distributed organization. Being in Portland is welcome, but we will not let geography keep us from the right person.

Email join@sigillogic.com with your resume or CV and a short note about the hardware, firmware, or formal-verification work you are proudest of. Links to code, papers, talks, or project artifacts are welcome but not required.

Learn more about Sigil Logic and HOARDE.