Ask HN: Can we translate normal Rust (axum) to Lean 4 without restrictions?

I'm trying to build a web app in Rust using axum, and am thinking whether I can export that Rust code to Lean4 so that I can verify business logic or security properties.

I first tried Aeneas, but it can only work for restricted grammer and structurs that are hard to review (it even doesnt look like Rust).

For example, when I want to write:

``` fn find_post(ps: &[Post], id: u64) -> Option<&Post> { ps.iter().find(|p| p.id == id) } ```

I have to write:

``` pub fn find_post(ps: &Vec<Post>, id: u64) -> Option<Post> { let mut i = 0; while i < ps.len() { if ps[i].id == id { return Some(ps[i].clone()); } i += 1; } None } ```

Is there anybody who have addressed this kind of problem??

For anyone interested, the experiment source and examples are at https://github.com/h5i-dev/i5h. I've ported parts of a few real web apps (e.g., Kellnr, Atuin, Wastebin, Conduit), and their core logic can now be verified to some extent. Ofcourse, that does assume the rest is correct, like axum/hyper for HTTP and PostgreSQL plus the engine for storage.