LiquidJava errors show verifier details and may include a hint, but it can still be difficult to understand why a refinement or state transition failed.
Add an Explain error action that uses a small model, such as Luna, to produce a short rationale and a useful next step. Ground the explanation in the diagnostic and relevant code, and display it separately from the verifier’s existing hint.
For a user study, investigate whether this can use a Copilot integration or a project-funded API key. Compare feasibility and cost before choosing a provider.
A prototype should cover refinement and state errors and make clear that the explanation is AI-generated.
LiquidJava errors show verifier details and may include a hint, but it can still be difficult to understand why a refinement or state transition failed.
Add an Explain error action that uses a small model, such as Luna, to produce a short rationale and a useful next step. Ground the explanation in the diagnostic and relevant code, and display it separately from the verifier’s existing hint.
For a user study, investigate whether this can use a Copilot integration or a project-funded API key. Compare feasibility and cost before choosing a provider.
A prototype should cover refinement and state errors and make clear that the explanation is AI-generated.