The Coq mailing list

[Gregory Malecha <gregory AT bedrocksystems.com>]

Hello coq-club --

I lead the formal methods team at Bedrock Systems (bedrocksystems.com) and we are looking to hire two full-time research engineers. An overview of the positions is at the bottom of this message; our operating systems and system security groups are also hiring and FM experience/background is highly valued in those roles as well :)

Formal methods are at the core of BedRock's business and we are deeply committed to solving problems of system verification at industrial scale. We get FM techniques and insights into the code early on and use them to build, maintain, and evolve code. This includes developing more agile techniques to keep evolving verified systems once they're built.

We have eight folks on the formal methods team today, hailing from MPI-SWS, MIT CSAIL, Princeton, and other leading research groups. If you're interested, send me an email or you can inquire more broadly at jobs AT bedrocksystems.com.

Company overview:

BedRock is building a trustworthy compute base for mission-critical applications. The foundation of the platform is an open source, multi-core, capability-based micro-hypervisor that we are developing and verifying. On top of these deep specifications we are writing and verifying applications to provide an extensible and configurable core.

Our contention is that the time is ripe for verifiably trustworthy systems, for everything from secure phones and industrial IoT to autonomous systems and financial infrastructure. With significant seed funding, great investors, and commercial projects underway, we are growing our team in Boston, the Bay Area, DC, and Germany.

Open Positions:

Proof Engineer

We are looking for a research engineer to help us formally verify our system. Our ideal candidate has a strong academic foundation coupled with real-world industry experience spanning proof assistants like Coq and LEAN, programming languages, operating systems, and C/C++.

• FM background is essential with either Coq, or LEAN secondary

• HOL/Isabelle may work but is not as close to our toolchain/method

Coding & systems engineering capability is a must

Knowledge of basic separation logic is a must, familiarity with the iris system is especially relevant

Industry experience is preferred

Proof Automation

We are looking for a research engineer who can help automate our proof toolchain and accelerate our “code-to-proof” loop. A strong foundation in proof automation and theorem provers is essential, along with a passion for verifying real-world systems and improving developer productivity. Coq, OCaml, compilers, and SAT/SMT solver experience is also pertinent.

• Ideally someone with Coq internals & hacking expertise who also has automatic theorem proving experience (including SMT/SAT) is highly desired

• if not Coq, something conceptually related/similar like LEAN is probably important

OCaml programming expertise is preferred

Strong conceptual foundation in proof assistants, automation, and theorem provers but who doesn’t have Coq experience could also be a good fit.

--

Gregory Malecha

Mail: gregory AT bedrocksystems.com

BedRock

Systems Inc
UNBREAKABLE FOUNDATION FOR

FORMALLY SECURED COMPUTING