20 ms·

Does formal verification stand up against logic flaws like this? I mean in theory, this thing functioned exactly as designed.

• otterley 5y ago
  I'm assuming, perhaps incorrectly, that the designers did not in fact intend for it to work this way.
  • smt88 5y ago
    You are incorrect. The system functioned as it was designed. This was an edge case that the designers didn't anticipate. In fact, this is a great illustration of why formal verification is not nearly sufficient to guarantee a properly functioning trading system.
    • allemagne 5y ago
      Are the statements: "the system functioned as designed" and "the system is not working as intended" mutually exclusive? I understand how the first can be arguable (or obvious, depending on what you mean), but are you really saying the second isn't true?
    • CuriousCosmic 5y ago
      This actually isn't quite correct. The original protocol actually had a formal spec that accompanied it. CreamFi chose to not maintain this spec. The spec constrained under what conditions the protocol could operate securely and (ignoring that their changes broke away from the spec) some of the tokens used in this and previous exploits to CreamFi did not meet those constraints. Had the team actually maintained the formal spec, they could have notified the listing committee (which every iteration of has had at least one team member on it). This was absolutely a human error however it likely would have been caught prior to entering production if the team had maintained the formal spec.