[Coq-Club] Positions at a startup company, using Coq to prove hardware

[Adam Chlipala]

I'm excited to announce opportunities for Coq hackers at the startup
company SiFive <https://www.sifive.com/>, for which I am a technical
advisor.

Briefly, SiFive offers a platform to help their customers create new
hardware solutions, combining off-the-shelf components like CPUs with
application-specific components.  They are very interested in assurance
about the correctness of such integration.  Their library of standard
components is centered on the very cool open instruction set RISC-V
<https://riscv.org/>, which was created by the founders of the company. 
They are located in Silicon Valley (California, USA).

SiFive is currently looking to hire a few Coq engineers to prove
correctness of processors and other crucial pieces of digital hardware. 
I believe all or most of these components will be open-source.  The
verification is being done using the Coq library Kami
<http://plv.csail.mit.edu/kami/> that began its life in my group at MIT,
partly under the umbrella of the DeepSpec <https://deepspec.org/>
project.  My former postdoc Murali Vijayaraghavan took a job at SiFive
to lead this effort.

I would encourage anyone interested in learning more to e-mail Murali
<mailto:***@sifive.com>.  Please be aware that these positions are
only open to people with nontrivial Coq experience, though experience
with hardware engineering is /not/ required.  (It all turns out to be
functional programming, anyway!)  In applying, please start by
summarizing your experience using Coq, ideally to demonstrate
correctness of (semi-)realistic systems.  The approximate bar is Coq
familiarity at the level we'd expect from doing a related master's
thesis.  However, there are also internship opportunities that may be
open to people with slightly less Coq experience.

[Murali Vijayaraghavan]

Just adding on to Adam's earlier advertisement about Coq-based verification
in SiFive.

You can also add your resumes directly in SiFive's job portal, specifically
for Coq-based verification, or send your resumes directly to me.
https://www.sifive.com/about/jobs/

Thanks
Murali

Post by Adam Chlipala
I'm excited to announce opportunities for Coq hackers at the startup
company SiFive <https://www.sifive.com/>, for which I am a technical
advisor.
Briefly, SiFive offers a platform to help their customers create new
hardware solutions, combining off-the-shelf components like CPUs with
application-specific components. They are very interested in assurance
about the correctness of such integration. Their library of standard
components is centered on the very cool open instruction set RISC-V
<https://riscv.org/>, which was created by the founders of the company.
They are located in Silicon Valley (California, USA).
SiFive is currently looking to hire a few Coq engineers to prove
correctness of processors and other crucial pieces of digital hardware. I
believe all or most of these components will be open-source. The
verification is being done using the Coq library Kami
<http://plv.csail.mit.edu/kami/> that began its life in my group at MIT,
partly under the umbrella of the DeepSpec <https://deepspec.org/>
project. My former postdoc Murali Vijayaraghavan took a job at SiFive to
lead this effort.
I would encourage anyone interested in learning more to e-mail Murali
to people with nontrivial Coq experience, though experience with hardware
engineering is *not* required. (It all turns out to be functional
programming, anyway!) In applying, please start by summarizing your
experience using Coq, ideally to demonstrate correctness of
(semi-)realistic systems. The approximate bar is Coq familiarity at the
level we'd expect from doing a related master's thesis. However, there are
also internship opportunities that may be open to people with slightly less
Coq experience.