I lead the formal methods team at Bedrock Systems (bedrocksystems.com) and we are looking to hire a full-time engineer working on automation in the Coq proof assistant (which is written in Ocaml). We’re very interested in candidates with strong Ocaml background especially in topics related to automated theorem proving, e.g. SAT/SMT solvers, datalog, superposition, resolution, etc. While Coq experience is great, you do not need to be a Coq expert to apply to this position, we’re happy to marry your Ocaml expertise with our Coq expertise.
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@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.