The Coq mailing list

[Gregory Malecha <gregory AT bedrocksystems.com>]

Hello --

BedRock Systems (https://www.bedrocksystems.com/, the website contains minimal technical information) is a new company applying the Coq proof assistant to develop verification tools, e.g. languages, compilers, and verification automation, as well as verified systems software, e.g. kernels, VMMs, and many other things. BedRock Systems is a young company, but we are very excited about applying formal methods to build high assurance systems and software. Much of our work is open source and we look forward to contributing back to the Coq community.

We are currently seeking formal methods experts in these areas to join our team in Cambridge, MA. We are especially interested in candidates with a strong Coq background. Experience reasoning about systems-level software and concurrency is a strong plus but is not essential.

If you are interested in the opportunity to work on hard problems and build real systems, please send me an email. We are seeking both interns (summer or any other time) and full time employees.

p.s. If this sort of thing interests you but you aren't looking for a job right now, please feel free to contact me, I'd love to talk about what we're doing and possible collaboration.

--

gregory malecha

gregory AT bedrocksystems.com

director of formal methods