Formal Modeling and Analysis of Legal Contracts using ContractCheck

on YouTube ↗23m

" summary

ContractCheck encodes Sales Purchase Agreements as structured blocks and translates them into decidable fragments of first‑order logic (SMT2) checked by the Z3 SMT solver. A pretzel bakery example shows a warranty timing contradiction: asserting a claim at day 29 conflicts with a 70‑day limitation, producing an unsat core; other queries yield satisfying models that show possible executions. Encoding is currently manual from ~1,400 pages of templates; future work aims to map text to blocks with machine learning and report partial MaxSMT solutions.

AI-written summary · about

" chapters (11)

1. 0:00Legal contract analysis intro
2. 2:31Detecting contract inconsistencies
3. 3:56Automated contract claim analysis
4. 5:22Building contract ontology
5. 7:09Formalizing warranty claims
6. 9:17Contract execution analysis types
7. 11:42Analyzing execution scenarios
8. 12:44SMT strengths in contracts
9. 13:48ContractCheck future research
10. 15:13Conclusion and key takeaways
11. 15:54Question and answer session