Formal verification

Mechanizing security-critical software, core algorithms, and structural properties using interactive proof assistants (Agda, Rocq, Lean) to eliminate bugs by mathematical certainty.

"Do not move fast and do not break things"

Formal methods in Blockchain

Mechanizing correctness/liveness proofs of smart contracts, decentralized ledgers, and distributed consensus protocols.

Compiler engineering

Developing translation pipelines, domain-specific languages (DSLs), and correct-by-construction code generation to bridge high-level specification and execution.

Formal methods in AI

Safeguarding AI systems through the use of dependent types and formal verification.

Functional programming

Designing expressive, type-safe software architectures utilizing Haskell and advanced type theory, alongside type-directed meta-programming techniques.

Information icon

We need your consent to load the translations

We use a third-party service to translate the website content that may collect data about your activity. Please review the details in the privacy policy and accept the service to view the translations.