Above all, we are researchers.
Founded by researchers and PhDs from INRIA, we publish in top venues, contribute to open-source ecosystems, and teach the technologies we create. Research is not a side activity. It is who we are.
Latest from the lab
Software Reliability: Systems Must Not Fail You at the Wrong Time
Discover how to ensure the software reliability of your critical systems and avoid costly outages through independent testing.
Legacy Systems: Your Greatest Undetected IT Risk (and How to Master It)
A system that has been running for fifteen years without a major incident is not necessarily reliable. Discover why legacy systems represent an invisible risk and how to manage it.
Fabrice Le Fessant on Digital Independence and Technological Sovereignty
Fabrice Le Fessant discusses digital sovereignty, open source, and building long-term European tech companies in an interview with La Jaune et la Rouge.
Recent research papers
Cross-Language Symbolic Runtime Annotation Checking
Zhicheng Hui, Léo AndrèsTail Modulo Cons, OCaml, and Relational Separation Logic
Clément Allain, Frédéric Bour, Basile Clément, François Pottier, Gabriel SchererL'explication par la paresse: Techniques d'évaluation hybrides à des fins d'explication de calculs
Louis GesbertRelational Abstractions Based on Labeled Union-Find
Dorian Lesbre, Matthieu Lemerre, Hichem Rami Ait-El-Hara, François BobotStorable types: free, absorbing, custom
Basile Clément, Gabriel SchererDeep expertise, from compiler to deployment
OCaml
Functional ProgrammingOur founding language. We build and maintain core OCaml tools, including the Flambda2 optimizing compiler, the opam package manager, and developer tooling used by the entire ecosystem.
Rust
Systems ProgrammingMemory-safe systems programming for performance-critical applications. We bring Rust into industrial codebases and train teams to adopt it confidently.
C
Low-Level & EmbeddedDeep expertise in C verification, static analysis, and testing. Our tools like SeaCoral provide automatic test generation and coverage analysis for safety-critical C code.
COBOL
Legacy ModernizationWe maintain GnuCOBOL and build SuperBOL Studio, the modern COBOL development environment. Sovereign migration paths from mainframes to open platforms.
WebAssembly
Portable ExecutionCross-language bug detection and symbolic execution through Owi, our WebAssembly analysis toolkit. Continuous analysis for C, C++, Rust, Zig, Go, and more.
Formal Methods
Mathematical VerificationAlt-Ergo SMT solver, Frama-C integration, and deductive verification. We prove software correct. Not just tested, but mathematically guaranteed.
Where we push the boundaries
Formal Verification
Proving software correctness through mathematical reasoning. We develop and apply SMT solvers, abstract interpretation, and deductive verification to ensure critical systems behave as intended.
Compiler Design & Optimization
Building and optimizing compilers for OCaml, COBOL, and domain-specific languages. From Flambda2's advanced inlining to GnuCOBOL's code generation, we push performance boundaries.
Programming Language Theory
Type systems, semantics, and language design. Our work on OCaml's type system, tail-modulo-cons optimization, and DSL design feeds directly into the tools we build.
Symbolic Execution
Automatic bug finding and test generation through symbolic analysis. Owi explores all execution paths of WebAssembly programs to find bugs that testing alone would miss.
Software Engineering & Tooling
Package managers, build systems, IDE extensions, and developer workflows. We create the infrastructure that makes programming languages usable at scale.
Academic collaborations
