We use cookies and other tracking technologies to improve your browsing experience on our site, analyze site traffic, and understand where our audience is coming from. To find out more, please read our privacy policy.

By choosing 'I Accept', you consent to our use of cookies and other tracking technologies.

We use cookies and other tracking technologies to improve your browsing experience on our site, analyze site traffic, and understand where our audience is coming from. To find out more, please read our privacy policy.

By choosing 'I Accept', you consent to our use of cookies and other tracking technologies. Less

We use cookies and other tracking technologies... More

Login or register
to apply for this job!

Login or register
to save this job!

Login or register to start contributing with an article!

Login or register
to see more jobs from this company!

Login or register
to boost this post!

Show some love to the author of this blog by giving their post some rocket fuel 🚀.

Login or register to search for your ideal job!

Login or register to start working on this issue!

Engineers who find a new job through Blockchain Works average a 15% increase in salary 🚀

Type Theorist & Formal Verification Engineer

Remote

16 November, 2020

Salary

Competitive

Contract type

Full time
Remote working

Technologies & frameworks

  • Dependent Types
  • Agda
  • Open Source
  • COQ
  • Formal Methods
  • Idris
  • Haskell
  • formal verification
  • agda2
  • formal language theory
  • type theory

Benefits & perks

  • Remote working
  • Flexible working
Smart contracts are not secure enough for finance, law, or systems engineering.

Role overview

Role overview

Smart contracts are security-critical, performance-sensitive, and bug-prone. Metastate is working on a dependently-typed smart contract language, Juvix, which utilises recent advancements in type theory to allow developers to write code in a high-level functional language, compile it to gas-efficient output VM instructions, and formally verify the safety of their contracts prior to deployment & execution.

PLT at Metastate focuses on applying the latest research in type theory and programming language design to concrete problems in the distributed ledger space. We are looking for a type theorist and formal verification engineer to work on various parts of the Juvix stack, all the way from formalisation of an operational semantics for the language in Agda to writing formally verified smart contracts in the Juvix language itself.

This role offers the chance to work closely with a small team on compelling cross-disciplinary problems in computer science, PLT, cryptography, and economics, and enjoy a high degree of independence in working conditions and prioritisation.

Responsibilities

  • Produce formal specifications and implementation plans for new language features in collaboration with team members (and optionally submit to academic venues)
  • Evaluate correctness, suitability, and ease-of-implementation of published type theory and PLT research for the Juvix architecture & project aims
  • Implement both in-house and published research in Haskell in the Juvix codebase in collaboration with team members
  • Conduct code reviews and help maintain a high standard of correctness and quality
  • Write production-ready formally verified smart contracts in the Juvix language itself for various purposes
  • Comprehensively document both design and implementation choices in the codebase, and assist in writing user-facing documentation for the Juvix language

Example subprojects & features

Qualifications

  • Prior experience in functional programming in Haskell, Idris, Agda, or Coq
  • Prior experience in formal verification or formalisation of a language
  • Self-motivated & self-organised
  • Interested in open-source technology and research applied to DLT

Bonus Qualifications

  • Prior academic work in type theory, PLT, or compiler design
  • Prior academic work in cryptography, economics, or game theory

Misc.

Competitive compensation in a negotiable mix of salary and equity.

Remote or local (Zürich/Zug, Berlin). When remote, preferred if mostly located within (+/- 7 hours) Central European time zones. Ideally someone who enjoys nature and hiking.

  • 10-49

Metastate is a research and engineering team focused on implementing cutting-edge research from numerous disciplines (distributed systems, PLT, zero-knowledge cryptography) and deploying them to solve hard problems in the blockchain space, such as scalability, secure smart contract languages, secure randomness or privacy. Metastate is a remote-first team, currently composed of 15 cross-disciplinary researchers and engineers located around the world. Our work culture is characterized by open-allocation, where team members have a high degree of freedom and autonomy in choosing when to work, what to work on, and whom to work with. Metastate was founded in early 2019 by @adrian_brink, @awasunyin and @cwgoes, with extensive experience in the blockchain space and who previously co-founded Cryptium Labs, a security-oriented proof-of-stake validator from the Swiss Alps.

View 6 jobs
Engineers who find a new job through Blockchain Works average a 15% increase in salary.

Salary

Competitive

Contract type

Full time
Remote working

Technologies & frameworks

  • Dependent Types
  • Agda
  • Open Source
  • COQ
  • Formal Methods
  • Idris
  • Haskell
  • formal verification
  • agda2
  • formal language theory
  • type theory

Benefits & perks

  • Remote working
  • Flexible working

Get hired!

Sign up now and apply for roles at companies that interest you.

Engineers who find a new job through Blockchain Works average a 15% increase in salary.

Start with GitHubStart with Stack OverflowStart with Email

Get hired!

Sign up now and apply for roles at companies that interest you.

Engineers who find a new job through Blockchain Works average a 15% increase in salary.

Start with GitHubStart with Stack OverflowStart with Email
Type Theorist & Formal Verification Engineer