Within Riverside Research, the Open Innovation Center (OIC) conducts internally funded and contract-funded R&D to develop technologies with lasting practical impact. The Secure and Resilient Systems (SRS) group within OIC focuses on rigorous approaches to building trustworthy computing systems.
SRS seeks a Research Scientist – Cryptography with an interest in formal methods to develop, prototype, and evaluate new formal methods techniques for software and systems security. The researcher will contribute to a range of collaborative R&D projects, working with colleagues across formal methods, cryptography, programming languages, and systems software.
If you are a cryptographer interested in programming language theory or formal methods as well as compilers, computer architecture, or operating systems, you should apply for this position. If you have mechanized cryptographic arguments in a theorem prover such as Rocq or Lean, or a verification tool such as CryptoVerif or EasyCrypt, you definitely should apply for this position. If you want to advance the state of the art in compositional, mechanized proofs of cryptographic protocol implementations, then you need to apply for this position!
Responsibilities- Conduct formal methods and cryptography research, including developing models, specifications, proofs, and verification techniques.
- Develop and evaluate research prototypes and tools that apply formal methods to software and systems security problems.
- Collaborate on multidisciplinary research with colleagues in formal methods, cryptography, programming languages, systems software, and related areas.
- Communicate research results through publications, reports, presentations, and briefings to technical and nontechnical audiences.
- Support research planning and proposal development by identifying new opportunities and contributing technical approaches.
- Bachelor’s degree in computer science, computer engineering, cybersecurity, or a related field; 5+ years of relevant research or engineering experience. Advanced degree preferred. Equivalent combinations of education and experience will be considered.
- Research experience in cryptography and a strong interest in formal methods, programming languages, or a closely related area.
- Experience developing or applying mechanized proofs or formal verification techniques.
- Demonstrated knowledge of cryptography, including techniques for reasoning about cryptographic security.
- Ability to formulate technical problems, evaluate alternative approaches, and conduct research independently and collaboratively.
- Ability to communicate complex concepts clearly in writing and in presentations, and to collaborate effectively with researchers from different disciplines.
- Ability to obtain and maintain a U.S. government security clearance.
- Experience with proof assistants or verification systems such as Rocq, Lean, Isabelle/HOL, EasyCrypt, F*, or similar tools.
- Experience with formal reasoning techniques such as game-hopping, universal composability, logical relations, translation validation, refinement, or separation logic.
- Experience formally verifying cryptographic implementations or protocols, compilers, operating systems, hypervisors, or other security-critical software.
- Familiarity with computer architecture, including topics such as tagged architectures, hardware/software interfaces, or ISA-level reasoning.
- Experience developing new formal methods tools or extending existing verification frameworks.
- A publication record or other demonstrated contributions to research in formal methods, security, cryptography, or programming languages.
Skills Required
- Bachelor's degree in computer science, computer engineering, cybersecurity, or a related field
- 5+ years of relevant research or engineering experience
- Advanced degree
- Research experience in cryptography and strong interest in formal methods, programming languages, or a related area
- Experience developing or applying mechanized proofs or formal verification techniques
- Demonstrated knowledge of cryptography, including reasoning about cryptographic security
- Ability to formulate technical problems, evaluate alternatives, and conduct research independently and collaboratively
- Ability to communicate complex concepts clearly in writing and presentations
- Ability to collaborate effectively with multidisciplinary researchers
- Ability to obtain and maintain a U.S. government security clearance
- Experience with proof assistants or verification systems such as Rocq, Lean, Isabelle/HOL, EasyCrypt, F*, or similar tools
- Experience with formal reasoning techniques such as game-hopping, universal composability, logical relations, translation validation, refinement, or separation logic
- Experience formally verifying cryptographic implementations, protocols, compilers, operating systems, hypervisors, or other security-critical software
- Familiarity with computer architecture, including tagged architectures, hardware/software interfaces, or ISA-level reasoning
- Experience developing new formal methods tools or extending verification frameworks
- Publication record or demonstrated contributions to formal methods, security, cryptography, or programming languages research
- U.S. citizenship
What We Do
Founded in 1967, Riverside Research is a not-for-profit organization chartered to advance scientific research for the benefit of the US government and in the public interest. Through our open innovation concept, we invest in multi-disciplinary research and development and encourage collaboration to accelerate innovation and advance science. Riverside Research conducts independent research in machine learning, trusted systems, optics and photonics, electromagnetics, plasma physics, radio frequency systems, and biomedical engineering. We move science from the laboratory to the field by building teams of recognized experts who deliver effective, high-value solutions and services to our customers. From public service to national security, we aspire to be a valued partner through our unwavering commitment to innovative and mission-focused solutions.









