Synthesis or Formal Verification Developer

• Contribute to YosysHQ’s synthesis or formal verification areas
• Develop and maintain tools using C++, Rust, and Python
• Work on implementation of hardware model checking and formal methods, or RTL/ASIC synthesis workflows
• Build software for engineering or science applications, implement algorithms from scientific literature, or work on compiler-related projects
• Become familiar with and contribute to a large pre-existing open-source project
• Take responsibility for assigned tasks and address challenges independently
• Contribute to Yosys and the open-source EDA ecosystem
• Potentially interact with or contribute to YosysHQ’s open-source tools

• Comfortable with C++ or Rust for formal verification; willingness to learn the other languages, including Python
• Familiarity with implementation of hardware model checking is ideal
• Alternatively, background in verification or formal methods such as SAT/SMT solving, automated/interactive theorem proving, programming language theory, or automata theory
• Some contact with RTL hardware design for formal verification
• Comfortable with C++ for synthesis
• Some experience with RTL hardware design, ideally for ASIC
• Experience building software for engineering or science applications, implementing algorithms from scientific literature, or working on a compiler may transfer to the role
• Experience becoming familiar with a large pre-existing project
• Ability to take responsibility for assigned tasks and work independently without extensive supervision
• Must not live in a country subject to sanctions or export restrictions, or be banned from performing work for the US government
• CV and brief cover letter required for application

• Flexible remote work
• Flexible working hours
• Part-time option (1–5 days per week)
• Flat pay hierarchy with the same rate for everyone
• Ability to work from wherever you are
• Team meetings usually between 3pm and 6pm Vienna time (CET/CEST), otherwise choose working hours