Leverage Our Unique Skillset and Experience to Succeed

With two decades of experience in building software products, we excel in delivering high-quality software and data engineering practices. Partner with us to turn your vision into reality and achieve outstanding results.

Hero

Technical Services

Instill confidence in your systems.

We collaborate with teams to ensure the security of their software and protocols both now and in the future.

We are a team of product, distributed systems and protocol experts renowned for detecting elusive bugs and errors in code and protocols. With deep expertise in protocol design, implementation, and analysis within the blockchain ecosystem, our roots trace back to the early days of Bitcoin, Ethereum, Cardano and Hyperledger, along with academic research on Byzantine fault-tolerant systems.

Manual Code Reviews

During code inspections, we manually analyze the source code to reconstruct the underlying protocols. The code acts as the definitive source of truth since it frequently diverges from specifications. Vulnerabilities are often found in codebases for various reasons

Protocol Analysis & Reconstruction

Protocol errors and bugs show up when rules are violated during its production execution. We perform audits to uncover these scenarios

End-to-End Vulnerability Testing

We analyse existing systems for any vulnerabilities. We uncover descrepencies between the documentation and their implementation

Our team brings decades of combined experience from both academia and industry in model checking complex systems protocols. We are the creators and maintainers of a user-friendly automated formal verification tool that we utilize in our security audits.

Adverserial Testing

Model checking is renowned for exposing unexpected edge cases in protocols. During "adversarial testing," we convert these edge cases into tests. Without advanced and thorough adversarial testing, systems are susceptible to numerous errors that jeopardize integrity and erode trust in the system. In such instances, protocol consensus engines can halt, leading to protocol crashes.

Formal Protocol Verification

Protocols in production often involve various distinct participants, leading to intricate protocol errors. To address this, we develop abstract formal descriptions of protocols using TLA+ to define the system and its attributes. We express the desired protocol properties as safety invariants and liveness conditions, and employ our proprietary model checking techniques to verify or refute them.

Model-Based Testing

We create test cases for the software we audit directly from TLA+ specifications. This significantly enhances manually developed test cases by incorporating those automatically generated from a formal model.