Hey all,

I just open-sourced Nona (https://github.com/jose-guillermo-rodriguez/nona), a #![no_std], zero-heap crypto engine built for AWS Nitro Enclaves over AF_VSOCK.

The core math, point operations, and memory boundaries are backed by 122 Verus proofs to make sure release binaries never touch the heap or panic at runtime.

For context on the build: my background is in facilities engineering and software QA rather than low-level cryptography. To put this together, I paired LLMs with Verus as a hard gate. If the solver couldn't prove the code against the spec, it got tossed out.

Everything builds and runs verification via make host or make all in the repo.

I’d really appreciate any feedback from the Rust community on the overall architecture, the #![no_std] setup, or blind spots I might have missed.

1 post - 1 participant

Read full topic