The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

I'm excited to announce opportunities for Coq hackers at the startup company SiFive, 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, 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 that began its life in my group at MIT, partly under the umbrella of the DeepSpec 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.  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.