The idea to formalize and link-up critical components in lean using LLMs like Amazon did for authorization, is quite compelling. This used to be cost-prohibitive. Now it may actually become a really great hard requirement to apply to an SBOM. 🤔
ping@SimpleStacker (as the only stacker I've seen to formulate proofs of functional ideas they offer on SN): do you have any thoughts about this approach where, when properly integrated, a formal proof can make for example fuzzing better? Like what Amazon did: simultaneously fuzz the production code and the proof, and check for mutual determinism.
The idea to formalize and link-up critical components in
leanusing LLMs like Amazon did for authorization, is quite compelling. This used to be cost-prohibitive. Now it may actually become a really great hard requirement to apply to an SBOM. 🤔ping@SimpleStacker (as the only stacker I've seen to formulate proofs of functional ideas they offer on SN): do you have any thoughts about this approach where, when properly integrated, a formal proof can make for example fuzzing better? Like what Amazon did: simultaneously fuzz the production code and the proof, and check for mutual determinism.