Informal Systems

Design and correctness assurance of distributed systems. In the blockchain space, Manuel is an expert in consensus protocols, blockchain interoperability, and L2 blockchain solutions. For correctness assurance, Manuel uses a variety of formal methods techniques, and tools: from mathematical analysis to model checkers and property-based testing via random simulation.

Formal analysis of safety-critical systems. Ivan’s background is in applying formal methods (FM) in systems that must not fail. He did his PhD on formal methods in robotic systems at Max Planck Institute for Software Systems. In the blockchain space, he is performing audits of Cosmos projects, applying the FM toolbox, which includes modeling in TLA+ and Quint, model checking, model-based testing, static analysis, and fuzzing. Where the toolbox is not applicable, he does not shy away from digging deep into the code to prove desired system properties or find their violations manually. Ivan also took part in developing Informal’s internal analysis tools, such as Atomkraft and Modelator.

Bringing a strong foundation in distributed systems, Mirel specializes in Cosmos blockchain security audits. Her core responsibilities include detailed code inspections and protocol analyses, with a focus on custom modules, CometBFT, and DEXs. A notable skill is crafting precise threat models to identify potential attack vectors. One additional strength is her ability to suggest improvements in design, architecture, and coding practices, enhancing both security and development. Mirel performs thorough code inspections and utilizes various testing approaches (unit tests, component tests and e2e testing) to detect and verify issues.