注意: これは過去の募集です。現在は募集をしておりません。新たに募集する場合は新しくお知らせ致します。
弊社ダイラムダ株式会社で一緒に働いてくださる方を若干名募集します。
ダイラムダとは
オフィスは京都大学のインキュベーションセンター内に入居している、「京大ベンチャー」です。現在、Tezosブロックチェーンに関する開発を行なっています。
Tezosとは
パブリック・ブロックチェーン技術です。次のような特徴があります:
- PoS (Proof of Stake)
- BitcoinのようなPoW(Proof of Work)と異なりエネルギーの浪費、マイナーとトークン保有者との動機の不一致のないPoSを採用しています。
- スマートコントラクト
- Turing完全、強い型付き、純粋関数型スタックマシンによるスマートコントラクト。
- プロトコル自己改訂
- プロトコルのアップグレード手続きはプロトコル自身に定められ、承認投票を通ると自動アップグレードされる。
現在、各暗号通貨の全流通額を米ドルに換算したマーケットキャップでは全通貨中で10位、PoSブロックチェーンではEOSの次にあります。(EOS は DPoS という厳密には PoS とは違った系統になるので、これを除くと PoS では1位になります。)
パブリック・ブロックチェーンは誰でもノードを立ててネットワークに参加できる分散データベースです。ノード間での合意形成を進め、悪意ある攻撃を防ぐために、データベース使用料、維持報酬として換金可能なトークンを介したインセンティブ設計がなされています。ブロックチェーンシステムを構成する、プロトコル、スマートコントラクト、アプリケーションに脆弱性があると、攻撃対象とされこのトークンを詐取される可能性があります。実際様々な詐取事件により巨額の経済的被害が発生しています。これを防ぐために Tezos では形式検証技術を積極的に使用してプログラムの安全性を保証していくことを重要視しており、そのプロトコルの実装は形式検証と相性の良い関数型言語 OCaml で書かれています。
Tezos の技術的なことは
を見てください。
ダイラムダのTezos開発
ダイラムダは Tezos のコア開発者として研究開発を Tezos財団から委託受けて、他のTezosコア開発者(Nomadic Labs, Cryptium Labs, LIGO)と共同で行なっています。
Plebeia ストレージ
現在ダイラムダが担当しているコア開発は Plebeia という Merkle Patricia tree の実装で、ブロックチェーン状態を Git に似た台帳方式で記録するための次世代ストレージシステムです。これも全て OCaml で書かれています。
ストレージシステムと言っても、ディスクアクセスという低レイヤーから、Merkle proof 生成というプロトコルの要となる trustless 技術にまで、パフォーマンスからセキュリティにまで渡る幅広い案件です。
Plebeia では基礎アルゴリズムの正しさを F* や Coq による証明を与えることを目標にしています。現在、基本的なツリー操作、Merkle ハッシュの衝突攻撃耐性などについての証明があります。
SCaml コンパイラ
SCaml は OCaml から Tezos スマートコントラクトのVM言語である Michelson へのコンパイラです。SCaml は OCaml のコンパイラフロントエンドをできるだけそのまま使い、言語として OCaml の厳密なサブセットになっているのが他の Tezos スマートコントラクト高級言語との一番の違いです。このデザインのおかげで、SCaml の実装はその言語機能に比べて非常に小さくまとまっており、OCaml のツール(Tuareg, Merlin, ocp-indent など)、ドキュメントがそのまま使えるという利点があります。表現力も十分ありFA1.2という Tezos 上でのトークン実装仕様も簡単に実装できます。
SCaml は単体のコンパイラとしては大体完成しています。SCaml が OCaml であることを活かし、スマートコントラクト、オフチェーンサーバ、クライアント、全てのプログラミングを OCaml 一言語で完結させることが可能です。また、Coq や F* から OCaml へ extraction を行うことで、正しさを検証したコードを SCaml でコンパイルし安全なスマートコントラクトを生成する、といった可能性のあるプロジェクトです。
SCamlの開発により、アプリ開発の知見を得ることができましたので、コア開発だけでなくTezos使用案件のお手伝いも可能になりました。
京都大学のTezosプロジェクトとの共同研究
Tezos のスマートコントラクトの検証を篩型を使って行う京都大学の ReFX チームと一緒に非公式ですが共同の研究活動も行なっています。
日本でのコミュニティ形成
Tezos は安全性も高く、科学的にも意義のあるプロジェクトですが、技術を使う人が増えなければただの投機対象に留まります。そのため、Tezosでは技術コミュニティ育成にも力を入れています。
日本での Tezos の普及活動もダイラムダの仕事の一部です。日本での Tezos 普及を担う一般社団法人 Tezos Japan と連携し、昨年度は十数回の講演、ハンズオンなどを行いました。なかなか人が集まれない昨今ですが、場所をネットワーク上に移行して活動を続けています。
弊社が行なった講演、ハンズオンの資料など。(性格上スライド間には重複あります。)
やらないこと
純粋なテック企業です。暗号通貨への投資、投機、およびその斡旋は行いません。社員にも推奨するつもりはありません。代表取締役は長年金融システム開発に関わってきましたが、金融投資よりは、クリティカルシステムを安全に開発することに興味があります。
社員募集
この一年半ほど、京都大学の末永幸平先生を顧問にお迎えし、proof ninja 社の今井宜洋さんという同志も得て上のような仕事をしてきましたが、やりたいことはあるのに手が足りない状態になってきました。そこで、これらの仕事を一緒にやってくださる方を募集します。
- 業務内容
- Tezos ブロックチェーンのコア、エコシステム開発。成果物はOSSとして公開します。
- Tezos ブロックチェーンを利用した国内/国外開発プロジェクトへの参画。
- 日本での Tezos コミュニティ活動(登壇、講師など)。得手不得手あると思いますが、極東の隔離環境で開発だけしているのは精神的に良くないので、できる範囲でやっていただきたく思います。
研究職ではありません。開発してアウトプットを出すのが第一目標です。余力があれば研究してください。
- Required skills
- OCamlプログラミング能力。業務はほぼ OCaml 系のコードを見ることになります。
- 日本語と英語の読み書き。会話。
- 理論計算機科学。修士以上が目安。論文読書き。
- マイクロマネージ不要な自主性と、蛸壺にハマって浪費する前に相談する勇気。
- FUDと高ボラティリティに惑わされない泰然。
- Plus
- OCamlでの業務、OSS開発経験。
- 形式検証技術。
- 言語処理系実装。
- コミュニティ活動への積極性。
- ブロックチェーン技術。(なくても一向に構いません)
- 基本勤務形態
- オフィスは京都ですが、現在の COVID-19 の状況下ではフルリモートです。
対面コミュニケーションはある程度必要だと思っていますので、COVID-19 収束後は、オフィスに通勤していただきます。毎日来ていただく必要はなく、在宅の方が多めでもいいと思っています。毎日出勤したい方はしていただいて構いません。
国内のミーティングは昼から夕方にあります。ヨーロッパとの会議が日本の深夜にある場合は、家からの参加をお願いします。プロトコルアップグレードのタイミングや、国際イベント参加の場合、週末、祝日の労働をお願いする場合があります。その場合後日お休みを取っていただきます。
全てのご要望にお応えすることはできませんが、基本以外の形がいいという方はご相談ください。
- 待遇
- ご経験・スキルを考慮して決定いたします。
応募、問い合わせ
contact@dailambda.jp に email してください。