Formal Methods Engineer

About the role

We apply formal methods, symbolic execution, and automated program analysis to find critical vulnerabilities in software before it ships. Our current domain is smart contracts, but the techniques are domain-agnostic and our roadmap is not limited to any single ecosystem.

We are hiring a Formal Methods Engineer to work on the analysis engine and tooling behind that work: the systems that infer invariants, attack them automatically, and deliver the results to developers who will never see the machinery underneath.

Prior experience with formal methods is not required. We regularly train engineers from mathematics, systems, and compilers backgrounds into this work, and we have found that mathematical maturity and curiosity predict success far better than familiarity with any particular tool.

Responsibilities

1. Design, build, and maintain the core analysis infrastructure: symbolic execution engines, solver integration, invariant inference, counterexample generation, and the pipelines that connect them.
2. Translate techniques used manually by our research team into automated, generalizable capabilities in the product.
3. Extend and optimize the application of symbolic execution, SMT solving, abstract interpretation, and model checking, including the performance and scalability work that determines whether these techniques are usable on real codebases.
4. Build the front-end of the analysis pipeline: front ends for new languages, compilers, and runtime platforms as we expand into new domains.
5. Design how results are surfaced, so that findings are actionable for developers without verification expertise.
6. Establish the testing, benchmarking, and regression infrastructure needed to know that the analysis engine is actually correct.

Required qualifications

1. Strong software engineering ability, with a track record of building and maintaining non-trivial production systems.
2. Demonstrated strength in at least one of the following areas:
3. Compilers and programming languages — experience with parsers, intermediate representations, type systems, interpreters, or language tooling. This background maps unusually well onto our work.
4. Mathematics or theoretical computer science — logic, proofs, formal reasoning, and constructing counterexamples.
5. Systems engineering — a working understanding of low-level software behavior and experience debugging complex systems.
6. Other deep-tech domains where correctness is a hard requirement rather than an aspiration.
7. Ability to reason carefully about unfamiliar systems and to state informal expectations in precise terms.
8. Clear technical communication, both written and verbal.

Preferred qualifications

1. Experience building developer tooling, static analysis frameworks, fuzzers, or compiler infrastructure.
2. Exposure to verification tooling such as SMT solvers, model checkers, or proof assistants.
3. Interest in cybersecurity, vulnerability research, or adversarial analysis, whether professional or self-directed.
4. Performance engineering experience on workloads where search space and solver time dominate.
5. Open-source contributions, publications, competition results, or comparable public work.

What we explicitly do not require

1. Prior formal methods experience. Most candidates with the backgrounds above do not have it.
2. Smart contract or blockchain experience. That is our current domain, not our identity, and the role is not tied to it.

Why this role

1. Theory applied to practice. Real mathematics applied to real code, with real consequences when it fails.
2. Genuinely open problems. Automatically inferring the correct invariants for an arbitrary codebase is unsolved, and the tooling is where that problem gets solved.
3. Compounding impact. Every improvement to the engine improves every subsequent analysis, rather than fixing one bug once.
4. Practitioner-led learning. You will learn formal methods from people who use them adversarially in production, not only in papers.