San Mateo, CA
Theorem Prover/Proof-Assistant Engineer
SiFive is looking for experts in proof-assistant based formal verification, who are passionate to apply their expertise to new domains. We are developing a radical approach to build hardware systems, by designing massively customizable hardware generators using a Coq-based DSL and use the theorem proving capabilities to prove full functional correctness of the designed generators, for all possible instances. The role spans from developing the proof infrastructure further to make it more automated and easier to use for proving complex invariants in hardware systems, which are highly concurrent, all the way to designing hardware and proving it correct. Knowledge about hardware systems is definitely a plus but is not required.
- Help drive the architectural definition, design, development and formal proof of hardware components;
- Innovate in novel applications of proof automation techniques to make formal proofs of hardware components easier and more automated;
- Help develop persistent interfaces to customizable hardware generators to enable components developed in Coq DSL to interact with other hardware generators seamlessly.
What you bring to the challenge
- Expertise in proof-assistant based formal verification methodologies and willingness to learn and use Coq;
- Proficient in intuitively identifying invariants in complex systems;
- Extreme rigor in logic and math to be able to prove complex theorems;
- Expertise in functional programming.
Nice to have
- Experience in computer architecture, designing processors and other hardware systems;
- Involved in developing Coq or some other proof assistant;
- Familiarity with Haskell and OCaml.
SiFive is proud to be an equal employment opportunity workplace. We offer a competitive compensation package that includes flexible paid time off, health, vision and dental benefits, 401(k) plan, employee stock option program, and much more. If you yearn to be challenged and wish to work in an environment where the boundaries of your creativity and skills will be tested, then SiFive is place for you.