Add verification coverage for all backends (either using existing or new methodologies)

[mkannwischer]

Identified during the 2026 soundness review (#1582, SOUNDNESS.md).

Not all backends (C reference, native aarch64, native x86_64) have equal verification coverage. Some backends may lack correctness, memory-safety, or constant-time proofs that are available for others. This gap means that the overall security guarantees depend on which backend is used.

Extend verification coverage to all backends, either by applying existing methodologies or developing new ones where needed.