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

Blog

• 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.
• You must buy SyncStitch with only 64,800 JPY!  ‒ October 15, 2018
  Dive into CSP (Communicating Sequential Processes) modeling.

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)