Metasepi maps Unix-like kernel design into the strongly-typed sea.

Blog

• Gave My First Talk About Takibi at OCaml Meeting 2026 in Tokyo  ‒ August 22, 2026
  Presentation "Create your own programming language and OS using OCaml, LLVM, and Generative AI -- accessible to everyone"
• ATS2 can avoid some of FreeBSD Problem Reports  ‒ April 19, 2021
  Mechanically avoid 12% of latest FreeBSD Problem Reports without code review.
• ATS2 and VeriFast avoid some of FreeBSD vulnerabilities  ‒ October 14, 2020
  Mechanically avoid 16% of latest FreeBSD vulnerabilities without code review.
• A toy translator C to ATS  ‒ July 19, 2019
  Try to translate IDIOMATIC C code into human readable ATS code.
• So long VeriFast, and see again ATS  ‒ November 13, 2018
  Shutdown Chiers iteration, and Come back to Bohai.

Links

• Source code
• Videos
• Mailing list
• Meetup in Japan

Sub Projects

• Takibi language is a embedded language to capture errors on compile-time
• Japanese translations about ATS, VeriFast, and F*
• Ajhc is a Haskell compiler for Arafura iteration (shutdowned)