To clarify the position, my concern isn't that the project is bad - it's that security engineering is a two-front war. You have to add new protections (memory safety) without breaking existing contracts (like ld.so behavior).

When a project makes 'big claims' about safety, less technical users might interpret that as 'production ready'. My caution is caused by the fact that modifying the runtime is high-risk territory where regressions can introduce vulns that are distinct from the memory safety issues you are solving.

The goal is to prevent the regression in the first place. I'm looking forward to seeing how the verification matures and rooting for it.