Our Services

Informal is a full-suite R&D institution that offers services including: Technical and Executive Education, Training, Consulting, and comprehensive Research & Development with a focus on blockchains, distributed systems, and formal verification.

Teach

Informal offers educational workshops for executives as well as technical training for in-house teams. Workshops are customizable in time and content according to your needs, and cover topics including Introduction to Blockchains, Tendermint & Cosmos, Distributed Systems and Formal Verification.

More Info Less Info

  • Two-Hour Introduction: Popular for executive training.
  • Half-Day Workshops: Popular for executive training.
  • Day-Long Workshop: Can be a deep dive or cover a wide range of modules. These courses can be adapted for a technical or non-technical audience.
  • Multi-Day Workshops: Multi-day customizable workshops. This offering is popular for technical training and hands on experimental development.

Modules

  • Blockchain
    • Introduction
    • How Bitcoin Works
    • How Ethereum Works
    • The CryptoCurrency Ecosystem
    • Proof of Work vs. Proof of Stake
    • Scalability
  • Tendermint & Cosmos
    • Tendermint Consensus, Networking, Interface and Applications
    • Cosmos Design, SDK, Applications, and Ecosystem
    • Inter-Blockchain Communication (IBC)
  • Distributed Systems
    • Introduction
    • Consensus Algorithms and State Machine Replication (SMR)
    • Implementations and Applications
  • Formal Verification
    • Introduction to formal verification of distributed systems
    • Modelling using TLA+
    • Model Checking Consensus Algorithms using TLC and Apalache
    • Verification Driven Development (VDD)

Assess

Informal can help your technical team with analysis of system architecture and protocols, performance improvements, formal specifications and verification, code review, automatic test generation, large scale adversarial testing, and more.

More Info Less Info

  • Consulting
    • High level architecture assessment
    • Performance improvements analysis
    • Protocol design and analysis
    • Formal specifications and verification
  • Audits
    • Code review and supplemental specification
    • Formal modelling and verification
    • Automatic test generation
    • Large scale adversarial testing
    • Large scale performance evaluation
    • Semantic code audits
  • Specification Writing
    • Designing and writing specifications for existing fault tolerant distributed protocols

Design

Using our Verification Driven Development methodology, Informal can help you gain confidence in the design of R&D projects, so you can save money and time by discovering problems during the design phase.

More Info Less Info

Design work may include:

  • Specification writing: Modelling distributed and concurrent algorithms and architectures using TLA+
  • Efficient model checking of systems specified in TLA+ using TLC and Apalache model checkers

Implement

Informal can help your company implement high-value distributed systems including; cryptocurrency platforms and blockchain frameworks, and integrations with Cosmos.

More Info Less Info

Implementation work may include:

  • Application Blockchain Interface (ABCI) for connecting blockchain applications on Tendermint consensus
  • Blockchain applications on Cosmos using SDK modules
  • Inter-Blockchain Communication Protocol (IBC) to connect different blockchains
  • Light Clients

More about our Verification Driven Development Methodology

Our VDD approach is a collaboration between researchers and engineers. It involves an iterative development of specifications and implementations, tooling to generate implementation tests from specifications, static analysis of code, and possibly other approaches.

How it works:

  • We start by specifying the system we want to develop.
  • Using formal methods, we test our design by formally verifying the system specification. This step reveals design problems early before any part of the system is implemented.
  • Once the design issues are corrected, the implementation of the formally specified system begins.
  • Using the formal specifications, we also generate test suites, which help verify the development during the implementation phase.
  • The result is a formally verified design, specification, tests, and implementation of the software. Ultimately demonstrating that verification upfront during the design phase can help develop reliable and robust distributed systems that are simpler to build and require less development and debugging time. Our VDD approach gives researchers and engineers strong confidence in the system they have designed and developed.