Research at Inferara
We research because we believe that the rigorous foundational justification and theoretical evaluation together form the key to future success. We do not speculate, rather, prove our thoughts by pedantic analysis of existing literature, publications, and other available sources.
Our Research Domains
Web3 Security
Web3 security domain consists of (but not limited) security of the blockchain code itself along with the DApps code security. And these two we consider as our research result target application area.
Mathematical Theorem Proving
Our work seeks to extend what is possible in automated reasoning systems and formal verification methods. We use Rocq (Coq) and TLA+ as our main tools.
Code Correctness
We concentrate on developing methodologies that ensure code operates exactly as intended, eliminating vulnerabilities and enhancing reliability. The approach we push is to use formal specifications and formal proofs for the critical code segments from the very first development stage.
Our Vision
We want to prove the formal properties of code on the models we develop using inductive reasoning.
We want to support abstract parameters as well as an instantiation of those parameters.
We want to build proofs in a minimalistic and clear way using a small trusted codebase; excluding machinery code generation.
We would like to have a framework that not only provides these things but also has good support for “programming in the large” and building abstractions.
If you share our passion for these topics and are interested in exploring collaborative research opportunities, we warmly invite you to reach out to us. Our team is eager to discuss potential partnerships and projects that can further advance the field. Please find our contact details on the main page, and let’s forge new frontiers together.