Example of simple formally verified computer program in Lean

Stream: lean4

[Miguel Negrão]

Is there an example of a simple formally verified computer program in Lean that I can have a look at ? Thanks !

[Siddhartha Gadgil]

If you want a tiny example: https://github.com/siddhartha-gadgil/proofs-and-programs-2023/blob/main/PnP2023/Lec_01_20/NatMin.lean

[Miguel Negrão]

Thanks, that's a great example ! I would be also curious to see something a bit bigger, like a web server, or similar, but not as big as the sel4 kernel.