It would be impractical. It would be monumental to even specify what 'safe' means in that degree of freedom, let alone allow/reject arbitrary assembly code according to the spec.
E.g. Trying to reject string operations which write beyond the trailing \0. At assembly level, \0 is only one of many possible conventions for bounding a string. E.g. maybe free() is allowed to write past 0s. So you'd need to decide whether it's safe depending on context.
Well yeah, I assumed if I was doing formal verification that that would necessarily involve fully specifying/tracking data sizes, which would mean that all strings would be pascal strings (at least internally; obviously it might be necessary to tack on a \0 for compatibility with external code).
E.g. Trying to reject string operations which write beyond the trailing \0. At assembly level, \0 is only one of many possible conventions for bounding a string. E.g. maybe free() is allowed to write past 0s. So you'd need to decide whether it's safe depending on context.