What is Formal Verification Machine assisted property verification of formal propositions. Comparison with Informal Verification (regular math proofs): FV leaves no ambiguity, IV needs human interpretation FV is checked by machine, IV is checked by (expert) (fragile) human FV is very verbose and cumbersome, IV is more succint and clean Uses of Formal Verification

Polygeist 8/16 bit arithmetic Modify the compiler so that all arithmetic operations happen at the lowest common denominator instead of always being raised to 32 bit arithmetic. HEIR Attributes removal Write a pass to remove func.func attributes. Then we can avoid this hack: cat main.mlir | sed 's/attributes {[^}]*}//g' > main-noattrs.mlir Remove unused functions