Smart contracts are not secure enough for finance, law, or systems engineering.
Smart contracts are security-critical, performance-sensitive, and bug-prone. Heliax 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 Heliax 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.
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 🏔️.