Anzenlang (安全言語) is specialized in software safety through language safety: strong-typing, formal verification, high language expressiveness… That’s why we love Lean 4 and Rust.

We mostly work with academics on language-related topics:

• DSL conception, compilation and verification, especially for (critical) embedded systems;

• theorem proving in Lean 4, for software safety and fundamental results;

• Lean 4, Rust, and formal verification training.

Legal notices (in French) / mentions légales.