takibi

Takibi is a research prototype consisting of a custom systems language and a corresponding monolithic kernel. The project aims to eliminate common kernel-level failures—such as buffer overflows, resource leaks, and context violations—by encoding these obligations directly into the type system. Key technical features include: - Language Design: Implements refinement types for proven array indices, affine and linear ownership for resource management, and an effect system to track execution contexts (e.g., blocking vs. interrupt contexts). - Compiler: Written in OCaml and utilizes LLVM 19 for native code generation. - Kernel Capabilities: The kernel is Linux-ABI compatible, allowing it to run existing AArch64 ELF binaries. It supports a subset of Linux syscalls, demand-grown page tables, copy-on-write, and an ext2 root filesystem. - Networking: Includes its own TCP/IP stack supporting ARP, IPv4/IPv6, ICMP, and TCP. - Hardware Support: Boots on QEMU/AArch64 and Raspberry Pi 5, capable of running Alpine BusyBox and serving files via HTTPd. The project serves as a research vehicle to explore how a language can be evolved to solve real-world systems programming problems, moving away from runtime traps toward static proofs of correctness.