Formal Methods Pitch (19.09.2024)

FORMAL.md

Problems:

• Even though we specify what is needed for the front-end with API and types we cannot enforce nor specify the business logic.
• We cannot be sure that our understanding of the business logic doesn't have flaws in the first place.
• We cannot enforce invariants.
• We cannot be sure that our implementation doesn't have bugs.

All we will have is a husk of the API with no value at all.

Solution

Introduction

This problem is very common and I believe is already solved with better tools and approaches. There is a field in computer science/programming industry that focuses on this problem — Formal Verification.

There are tools for this, such as TLA+, Coq, Agda, Lean, CompCert. And in my opinion, TLA+ fits best our use case and team.

Well, this might seem like a very obscure, niche and new stuff. You might think that these tools might just be supported by only enthusiasts and used by noname companies. But I assure you — this is not the case. Formal Verification and these tools are already adopted widely by the industry long time ago. For example, Amazon uses TLA+ and here is the paper that they wrote about it: https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf. There are countless other examples for industry adoption, such as Boeing using Coq to verify the software of their planes, etc. If you're still not convinced, take a look: https://github.com/ligurio/practical-fm.

How does TLA+ work?

When developing software, there are two main stages:

1. Gathering requirements from the client and building Technical Assignment (English: TA; Russian: ТЗ)
2. Actually developing the software according to that TA.

Doing as much as we can to understand the logic is our main goal before writing a single line of code. If we were not careful before the step 2 we end up with conflicting requirements, misunderstandings, correctness issues. Heck, sometimes we don't realize that we missed out something until we actually need it in the last 1-2 weeks of development. I think we remember that incident with Pool Balance in the project Inan. The most important thing in any bank - balance. But funny thing is - we didn't realize it until the end.

In order to prevent situations like these we need to build the Formal Specification of the TA before actually developing the actual software. This is where TLA+ comes in handy. We write out ALL OF OUR LOGIC, REQUIREMENTS and INVARIANTS in TLA+. After doing that we let the TLA+ verify it mathematically. If everything is alright with our logic and requirements we will have a FORMALLY VERIFIED SPECIFICATION. If it is formally verified, there is no damn way it is incorrect. One of the biggest benefits is - if we have formally verified specification we won't need any further explanations, meetings and others. Because everything will be in that specification. This should speed up the development too, because we won't have bugs because someone forgot some invariant in the logic.

Does it take a lot of time? No. We are not writing any implementation and therefore no need to setup servers, databases, authentication, CI/CD, tests and all those time consuming tests while writing the specification. We are thinking ABOVE THE CODE. Our main goal is to verify our logic.

So, our development iteration will be:

1. Gathering requirements from the client and building Technical Assignment (English: TA; Russian: ТЗ)
2. Verifying that every requirement makes sense and prove it mathematically.
3. Actually developing the software according to that formally verified spec. ...
4. Profit???

Recommendations

https://p-org.github.io/P/ https://quint-lang.org/ Alloy

Pros

• Helps us to verify the logic from the get go.

  • Helps us to detect the problematic logic earlier and decreases the feedback loop time.

• Helps us to safely make new changes to the logic.

• Saves time, by eliminating needs for meetings and chats with PM. We have the formal spec. We're good to go.

• Huge industry adoption.

• Old and stable technology.

• Good documentation, tutorials, books and communities making the learning easier.

• Prevents big fuckups in important projects. Such as Inan that manipulates money and most of it's logic is in mathematical calculations. It won't fail fast at all if there is a mistake -- it will continue with invalid state making the situation worse as the time passes.

• Eliminates the difference in terminology with PM, Backend & Frontend.

Cons

• Takes some time to learn.
• Familiarity bias makes it hard to get used to these technologies.

---

Readability - subjective. Correctness - objective.

profit.als

sig Contract {
  // input
  markup: Int,
  cost: Int,
  expenses: Int,
  bonus: Int,
  downpayment: Int,
  // computed
  spent: Int,
  bonusAmount: Int,
  profit: Int,
  total: Int,
  // accumulated
  var paid: Int,
  var realized: Int,
  var unrealized: Int,
}

fact calculations {
  all c : Contract | {
    // capping the limits
    c.markup >= 0
    c.cost >= 0
    c.expenses >= 0
    c.bonus >= 0 and c.bonus <= 100

    // dependent constraints
    c.markup >= c.bonusAmount + c.expenses // otherwise the profit will become negative
    c.downpayment <= c.cost // otherwise the cost will become negative

    // formula
    c.spent = c.cost - c.downpayment
    c.bonusAmount = mul[c.markup - c.expenses, div[c.bonus, 100]]
    c.profit = c.markup - c.bonusAmount - c.expenses
    c.total = c.spent + (c.markup - c.bonusAmount) + c.expenses

    // temporal
    always (c.realized = mul[c.profit, div[c.paid, c.total]])
    always (c.unrealized = mul[c.profit, 1 - div[c.paid, c.total]])
  }
}

assert profit_positive {
  all c : Contract | c.profit >= 0
}

assert realized_positive {
  always (all c : Contract | c.realized >= 0)
}

assert bonus_reasonable {
  all c : Contract | c.bonusAmount <= c.markup
}

assert profit_balance {
  always (all c : Contract | c.realized + c.unrealized = c.profit)
}

assert paid_underflow {
  always (all c : Contract | c.paid >= 0)
}

check profit_positive for 8 Int
check realized_positive for 8 Int
check bonus_reasonable for 8 Int
check profit_balance for 5 Int