High Assurance Software for Financial Regulation and Business Platforms
summary
An open stack called Morphir compiles Elm and Legend into a pure, loop‑free MorphirIR that maps one‑to‑one to SMT theories and is checked with SMT/Z3 encodings (nats as bitvectors, decimals, constructors). The pipeline finds real bugs like division‑by‑zero and generates concrete witnesses, scales to a few thousand lines with few timeouts, and uses bitvector bounding plus incremental widening and fuzzing as fallbacks while supporting pluggable checkers.
AI-written summary · about
chapters (18)
- 0:00Introduction
- 0:47Financial Technology Sector
- 2:23Surfboard Rental
- 2:58Liquidity Reporting
- 5:12Collaboration
- 7:06Morpher Platform
- 9:01Counter Example
- 9:38System Architecture
- 10:44MorpherIR
- 16:03Checker Workflow
- 18:04Checker Flow Diagram
- 19:24Frontend Languages
- 20:28Pluggable Checking
- 21:46Userdefined assertions
- 23:07Specialized checking
- 24:25Conclusion
- 25:14Links
- 26:01Questions
related talks
22mMorphir: A Single Language for Business and Technology
32mPanel: Integrating Legend, Bosque, and Morphir For Open Reg Tech through FINOS
38mAgile and Dependable Service Development with Bosque and Morphir
21mMOLA: A Runtime Verification Engine Factory by (Meta-)interpreting Embedded DSLs
29müberSpark: Enforcing Verifiable Object Abstractions for Automated...
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...
11mMorello Cerise: proving secure encapsulation (work in progress)
01h 05mVerifying Infinitely Many Programs at Once