eBPF is a revolutionary technology, which can be used to add additional capabilities to the kernel without changing the kernel source code or implementing kernel modules. The kernel is a critical part of the computer and requires extra precautions to ensure safety and avoid manhandling of the privileged data. To ensure this safety, the toolchain of eBPF includes a verifier, which ensures safety requirements before loading the program in the kernel. However, various research findings and experiments have proved that the verifier needs to be stronger in ensuring safety than it claims. A significant amount of work has been done to improve the capabilities of the verifier, and it is still an ongoing challenge. We propose a new eBPF programming language called BeePL, whose type system encodes the eBPF specifications and a formally verified compiler that preserves the properties until the BPF bytecode.