Role |
AI Engineer |
Formal Methods & Software Correctness |
Compensation |
$150k - $200k |
Offers Equity |
Location |
Flexible |
PT overlap required |
Apply |
[email protected] |
Send me your best work |
About Us
Workers IO (workers.io) is building AI agents that verify and enforce software correctness. We combine formal methods, program analysis, and practical tooling to help engineering teams ship reliable software with machine‑checkable evidence of correctness.
Role Summary
We’re seeking a hands‑on Engineer to design and build models that automate software verification. You’ll integrate LLMs with static analysis, model checking, symbolic execution, and contract systems to produce proofs, test artifacts, and compliance reports that stand up in real‑world certification environments.
Key Responsibilities
- Design AI agents that orchestrate verification pipelines (e.g., static analyzers, model checkers, symbolic executors, fuzzers, SMT solvers) to check properties such as memory safety, timing, concurrency, and interface contracts.
- Specify and validate properties by extracting or authoring pre/postconditions, invariants, and temporal properties.
- Integrate with embedded toolchains (C/C++/Rust, cross‑compilers, RTOS, simulators/HIL) and CI/CD to generate machine‑readable verification artifacts and traceability.
- Build evaluation suites and metrics (proof‑obligation discharge rate, soundness/precision, coverage, false‑positive/negative rates) and drive continuous improvement.
- Collaborate with domain experts in safety‑critical industries to translate requirements and standards into verifiable specifications and automated checks.
- Contribute code and tooling (libraries, plugins, benchmarks) and, where appropriate, open‑source components.
Minimum Qualifications
- BS or MS in Computer Science, Electrical/Computer Engineering, or related field or equivalent industry experience. (Degree is not required)
- Strong programming skills in verification aware languages and at least one systems language (C/C++ or Rust).
- Practical experience with one or more of: static analysis, abstract interpretation, SMT/SAT (e.g., Z3), model checking (e.g., TLA+), symbolic execution, runtime verification, or contract‑based design (e.g., Dafny).
- Experience building production‑grade developer tools or infrastructure (tests, CI, reproducible builds).