diff --git a/frontend/src/App.css b/frontend/src/App.css
index e27524814..bb3c7c6c8 100644
--- a/frontend/src/App.css
+++ b/frontend/src/App.css
@@ -1,21 +1,52 @@
 .App {
   text-align: center;
+  min-height: 100vh;
+  background-color: #fafafa;
+}
+
+/* Toolbar below header */
+.app-toolbar {
+  display: flex;
+  justify-content: flex-end;
+  padding: 12px 24px;
+  background-color: #f0f0f5;
+  border-bottom: 1px solid #ddd;
 }
 
 /* New Proof Button */
 .new-proof-btn {
-  position: absolute;
-  top: 20px;
-  right: 20px;
-  padding: 10px 20px;
+  padding: 9px 20px;
   font-size: 1rem;
   border: none;
   border-radius: 4px;
   background-color: #007bff;
   color: #fff;
   cursor: pointer;
+  transition: background-color 0.2s;
 }
 
 .new-proof-btn:hover {
   background-color: #0056b3;
 }
+
+.new-proof-btn:focus {
+  outline: none;
+  box-shadow: 0 0 0 3px rgba(0, 123, 255, 0.4);
+}
+
+/* Main content area */
+.app-main {
+  padding: 0 16px 40px;
+}
+
+/* Empty proof placeholder */
+.empty-proof-state {
+  margin: 40px auto;
+  max-width: 500px;
+  padding: 32px;
+  background-color: #fff;
+  border: 2px dashed #ccc;
+  border-radius: 8px;
+  color: #888;
+  font-size: 1.1rem;
+}
diff --git a/frontend/src/App.tsx b/frontend/src/App.tsx
index 881bbd077..e875c2acb 100644
--- a/frontend/src/App.tsx
+++ b/frontend/src/App.tsx
@@ -50,15 +50,31 @@ function App() {
     setColorMapping(new Map<number, string>())
   };
 
+  const hasProof = proof.goal !== '' || proof.steps.length > 0;
+
   return (
     <div className="App">
       <Header />
-      <button className="new-proof-btn" onClick={handleOpenModal}>
-        New Proof
-      </button>
-      <Menu logic={LOGIC} proof={proof} setProof={setProof} onColorChange={onColorChange} />
-      <Proof proof={proof} coloring={colorMapping} />
-      
+      <div className="app-toolbar">
+        <button
+          className="new-proof-btn"
+          onClick={handleOpenModal}
+          aria-label="Start a new proof"
+        >
+          New Proof
+        </button>
+      </div>
+      <main className="app-main">
+        <Menu logic={LOGIC} proof={proof} setProof={setProof} onColorChange={onColorChange} />
+        {hasProof ? (
+          <Proof proof={proof} coloring={colorMapping} />
+        ) : (
+          <div className="empty-proof-state" role="status">
+            <p>No proof loaded. Click <strong>New Proof</strong> to begin.</p>
+          </div>
+        )}
+      </main>
+
       <NewProofModal
         isOpen={isModalOpen}
         onClose={handleCloseModal}
diff --git a/frontend/src/components/Expressions.css b/frontend/src/components/Expressions.css
index 6d9f132ec..4246dccb9 100644
--- a/frontend/src/components/Expressions.css
+++ b/frontend/src/components/Expressions.css
@@ -11,35 +11,30 @@
     width: 100%;
     border-collapse: collapse;
     margin: 20px auto;
-    /* Top and bottom margin, auto for left and right */
     padding: 0;
-    /* Reset padding to avoid unwanted spacing */
     max-width: 1200px;
-    /* Optional: limit table width */
 }
 
 .proof-viewer th,
 .proof-viewer td {
     border: none;
-    /* No borders */
-    padding: 4px 8px;
-    /* Reduced padding for closer lines */
+    padding: 6px 12px;
     text-align: left;
 }
 
 /* Header Styles */
 .proof-viewer th {
     background-color: #f4f4f4;
-    color: #333;
+    color: #555;
     text-align: center;
-    /* Center align headers */
-    font-size: 3rem;
-    /* Larger header text size to match expressions */
+    font-size: 1rem;
+    text-transform: uppercase;
+    letter-spacing: 0.08em;
+    border-bottom: 2px solid #ddd;
 }
 
 .proof-viewer td.rule {
     text-align: right;
-    /* Right align for rule column cells */
 }
 
 /* Expression and Rule Styles with Preformatted Text */
@@ -47,31 +42,32 @@
     margin: 0;
     font-family: "Courier New", Courier, monospace;
     white-space: pre;
-    font-size: 3rem;
-    /* Large text for expressions */
-    line-height: 1.2;
-    /* Adjust line height to keep it tight */
+    font-size: 1.4rem;
+    line-height: 1.4;
 }
 
-/* Make Line Numbers and Rules As Big As Expressions */
+/* Line numbers and rule cells */
 .proof-viewer td {
-    font-size: 3rem;
-    /* Large text for both line numbers and rules */
-    line-height: 1.2;
-    /* Keep line height tight for uniformity */
+    font-size: 1.4rem;
+    line-height: 1.4;
+    vertical-align: middle;
 }
 
 /* No Alternate Row Colors */
 .proof-viewer tbody tr {
     background-color: transparent;
-    /* Keep the background consistent */
 }
 
-/* Highlight Rows on Hover */
+/* Subtle hover for rows */
+.proof-viewer tbody tr:hover {
+    background-color: #f5f5f5;
+}
+
+/* Highlight Rows on Hover (rule reference) */
 .proof-viewer tbody tr.highlighted {
-    background-color: #000; /* Black background */
-    color: #ff69b4; /* Pink color for the text */
-    font-weight: bold; /* Make the font thick */
+    background-color: #1a1a2e;
+    color: #ff69b4;
+    font-weight: bold;
 }
 
 /* Heading Styles */
@@ -88,9 +84,20 @@ h3 {
     color: #444;
 }
 
-  .glow {
-    box-shadow: inset 0 0 10px var(--glow-color), 
-                inset 0 0 20px var(--glow-color), 
+.glow {
+    box-shadow: inset 0 0 10px var(--glow-color),
+                inset 0 0 20px var(--glow-color),
                 inset 0 0 30px var(--glow-color);
-  }
-  
\ No newline at end of file
+}
+
+/* Proof wrapper and divider */
+.proof-viewer-wrapper {
+    max-width: 1200px;
+    margin: 0 auto;
+}
+
+.proof-divider {
+    border: none;
+    border-top: 2px solid #333;
+    margin: 0;
+}
diff --git a/frontend/src/components/Header.css b/frontend/src/components/Header.css
new file mode 100644
index 000000000..72fd01e9d
--- /dev/null
+++ b/frontend/src/components/Header.css
@@ -0,0 +1,15 @@
+.app-header {
+  background-color: #1a1a2e;
+  padding: 16px 24px;
+  display: flex;
+  align-items: center;
+  justify-content: center;
+}
+
+.app-title {
+  margin: 0;
+  font-size: 1.6rem;
+  font-weight: 600;
+  color: #e0e0ff;
+  letter-spacing: 0.03em;
+}
diff --git a/frontend/src/components/Header.tsx b/frontend/src/components/Header.tsx
index abbe4f893..86bcc2931 100644
--- a/frontend/src/components/Header.tsx
+++ b/frontend/src/components/Header.tsx
@@ -1,7 +1,12 @@
 import React, { FC } from 'react';
+import './Header.css';
 
 const Header: FC<{}> = () => {
-  return <h1>NATURAL DEDUCTION APPLICATION</h1>;
+  return (
+    <header className="app-header">
+      <h1 className="app-title">Natural Deduction Proof Assistant</h1>
+    </header>
+  );
 };
 
-export default Header;
\ No newline at end of file
+export default Header;
diff --git a/frontend/src/components/menu/Menu.css b/frontend/src/components/menu/Menu.css
index 2a553df55..00844ed45 100644
--- a/frontend/src/components/menu/Menu.css
+++ b/frontend/src/components/menu/Menu.css
@@ -10,6 +10,14 @@
     font-family: Arial, sans-serif;
 }
 
+/* Empty state */
+.empty-state {
+    font-size: 1.1rem;
+    color: #666;
+    margin: 0;
+    padding: 10px 0;
+}
+
 /* Label for Select */
 .menu-label {
     display: block;
@@ -27,6 +35,13 @@
     border-radius: 4px;
     margin-bottom: 20px;
     background-color: #fff;
+    cursor: pointer;
+}
+
+.menu-select:focus {
+    outline: none;
+    border-color: #007bff;
+    box-shadow: 0 0 0 3px rgba(0, 123, 255, 0.2);
 }
 
 /* Input Container */
@@ -56,7 +71,13 @@
     border: 1px solid #ccc;
     border-radius: 4px;
     outline: none;
-    transition: box-shadow 0.3s ease;
+    box-sizing: border-box;
+    transition: box-shadow 0.3s ease, border-color 0.2s;
+}
+
+.input-field:focus {
+    border-color: #007bff;
+    box-shadow: 0 0 0 3px rgba(0, 123, 255, 0.2);
 }
 
 /* Glowing Input Field */
@@ -67,9 +88,22 @@
 
 /* No Inputs Message */
 .no-inputs {
-    font-size: 1.2rem;
+    font-size: 1.1rem;
     color: #666;
     margin-bottom: 20px;
+    font-style: italic;
+}
+
+/* Inline error message */
+.menu-error {
+    color: #c0392b;
+    background-color: #fdecea;
+    border: 1px solid #f5c6cb;
+    border-radius: 4px;
+    padding: 8px 12px;
+    font-size: 1rem;
+    margin-bottom: 12px;
+    text-align: left;
 }
 
 /* Action Button */
@@ -84,6 +118,17 @@
     transition: background-color 0.3s ease;
 }
 
-.menu-button:hover {
+.menu-button:hover:not(:disabled) {
     background-color: #0056b3;
 }
+
+.menu-button:focus {
+    outline: none;
+    box-shadow: 0 0 0 3px rgba(0, 123, 255, 0.4);
+}
+
+.menu-button:disabled {
+    background-color: #9ec5fe;
+    cursor: not-allowed;
+    opacity: 0.7;
+}
diff --git a/frontend/src/components/menu/Menu.tsx b/frontend/src/components/menu/Menu.tsx
index f5dd94911..7d83380c0 100644
--- a/frontend/src/components/menu/Menu.tsx
+++ b/frontend/src/components/menu/Menu.tsx
@@ -38,7 +38,7 @@ function parseAction(
                     <GlowingInput
                         key={index+input}
                         index={index}
-                        label={input === 'int' ? 'Enter line number:' : 'Enter expression:'}
+                        label={input === 'int' ? 'Line number:' : 'Expression:'}
                         glowColor={glowingColors[index]}
                         onColorChange={onColorChange}
                         onInput={onInput}
@@ -46,7 +46,7 @@ function parseAction(
                     />
                 ))}
             </div>
-        ) : <p className="no-inputs">No inputs needed</p>
+        ) : <p className="no-inputs">No additional inputs needed</p>
     };
 }
 
@@ -55,6 +55,8 @@ const Menu: FC<MenuProps> = ({ logic, onColorChange, setProof, proof }) => {
     const [selectedAction, setSelectedAction] = useState<string>('');
     const [sources, setSources] = useState<number[]>([]);
     const [expression, setExpression] = useState<string>("");
+    const [errorMessage, setErrorMessage] = useState<string>('');
+    const [isLoading, setIsLoading] = useState(false);
 
     const selectedInputs = useMemo(() => {
         return actions.find(action => action.name === selectedAction)?.inputs || null;
@@ -63,6 +65,7 @@ const Menu: FC<MenuProps> = ({ logic, onColorChange, setProof, proof }) => {
     const handleActionChange: ChangeEventHandler<HTMLSelectElement> = (event) => {
         const newAction = event.target.value;
         setSelectedAction(newAction);
+        setErrorMessage('');
 
         glowingColors.forEach((color) => onColorChange(color,-1));
 
@@ -73,11 +76,12 @@ const Menu: FC<MenuProps> = ({ logic, onColorChange, setProof, proof }) => {
         } else {
             setSources([]);
         }
-        setExpression('');  // Reset expression
+        setExpression('');
     };
 
     const onInput = useCallback(
         (index: number, input: number | string) => {
+            setErrorMessage('');
             if (typeof input === 'number') {
                 setSources(prevSources => {
                     const newSources = [...prevSources];
@@ -100,6 +104,8 @@ const Menu: FC<MenuProps> = ({ logic, onColorChange, setProof, proof }) => {
 
     const processAction = () => {
         if (selectedAction === '') return;
+        setErrorMessage('');
+        setIsLoading(true);
 
         const actionDto: ActionDto = {
             name: selectedAction,
@@ -108,31 +114,57 @@ const Menu: FC<MenuProps> = ({ logic, onColorChange, setProof, proof }) => {
         };
 
         applyAction(logic, proof, actionDto, (response: ApplyActionResponse) => {
+            setIsLoading(false);
             if (response.success) {
                 setProof(response.proof);
                 glowingColors.forEach((color) => onColorChange(color,-1));
             } else {
-                console.error('Action failed:', response.message);
-                alert(`Action failed: ${response.message}`);
+                setErrorMessage(response.message || 'Action could not be applied.');
             }
         });
     };
 
+    const noProof = proof.steps.length === 0 && !proof.goal;
+
     return (
         <div className="menu">
-            <label htmlFor="action-select" className="menu-label">Select Inference Rule:</label>
-            <select id="action-select" className="menu-select" value={selectedAction} onChange={handleActionChange}>
-                <option value="">-- Choose an action --</option>
-                {actions.map((action, index) => (
-                    <option key={action.name} value={action.name}>
-                        {action.name}
-                    </option>
-                ))}
-            </select>
-            {selectedInputs}
-            <button className="menu-button" onClick={processAction} disabled={selectedAction === ''}>
-                Perform Action
-            </button>
+            {noProof ? (
+                <p className="empty-state">
+                    Click <strong>New Proof</strong> to get started.
+                </p>
+            ) : (
+                <>
+                    <label htmlFor="action-select" className="menu-label">Select Inference Rule:</label>
+                    <select
+                        id="action-select"
+                        className="menu-select"
+                        value={selectedAction}
+                        onChange={handleActionChange}
+                        aria-label="Select inference rule"
+                    >
+                        <option value="">-- Choose a rule --</option>
+                        {actions.map((action) => (
+                            <option key={action.name} value={action.name}>
+                                {action.name}
+                            </option>
+                        ))}
+                    </select>
+                    {selectedInputs}
+                    {errorMessage && (
+                        <p className="menu-error" role="alert" aria-live="assertive">
+                            {errorMessage}
+                        </p>
+                    )}
+                    <button
+                        className="menu-button"
+                        onClick={processAction}
+                        disabled={selectedAction === '' || isLoading}
+                        aria-disabled={selectedAction === '' || isLoading}
+                    >
+                        {isLoading ? 'Applying…' : 'Apply Rule'}
+                    </button>
+                </>
+            )}
         </div>
     );
 };
diff --git a/frontend/src/components/menu/__test__/Menu.test.tsx b/frontend/src/components/menu/__test__/Menu.test.tsx
index 274c9fef9..8ddfe6340 100644
--- a/frontend/src/components/menu/__test__/Menu.test.tsx
+++ b/frontend/src/components/menu/__test__/Menu.test.tsx
@@ -50,7 +50,6 @@ describe('Menu Component', () => {
 
     beforeEach(() => {
         jest.clearAllMocks();
-        global.alert = jest.fn();
     });
     
     test('renders Menu component and fetches actions', async () => {
@@ -64,7 +63,7 @@ describe('Menu Component', () => {
 
         await waitFor(() => {
             expect(screen.getByLabelText(/Select Inference Rule:/i)).toBeInTheDocument();
-            expect(screen.getByText('-- Choose an action --')).toBeInTheDocument();
+            expect(screen.getByText('-- Choose a rule --')).toBeInTheDocument();
             expect(screen.getByText('Action1')).toBeInTheDocument();
             expect(screen.getByText('Action2')).toBeInTheDocument();
         });
@@ -82,7 +81,7 @@ describe('Menu Component', () => {
 
         // Wait for the input fields to appear
         await waitFor(() => {
-            const inputFields = screen.getAllByLabelText(/Enter line number:/i);
+            const inputFields = screen.getAllByLabelText(/Line number:/i);
             expect(inputFields.length).toBe(2); // Expecting 2 input fields for Action1
         });
     });
@@ -96,7 +95,7 @@ describe('Menu Component', () => {
 
         fireEvent.change(screen.getByLabelText(/Select Inference Rule:/i), { target: { value: 'Action1' } });
 
-        expect(screen.getByRole('button', { name: /Perform Action/i })).not.toBeDisabled();
+        expect(screen.getByRole('button', { name: /Apply Rule/i })).not.toBeDisabled();
     });
 
     test('calls applyAction with correct parameters and updates proof', async () => {
@@ -118,13 +117,13 @@ describe('Menu Component', () => {
             fireEvent.change(screen.getByLabelText(/Select Inference Rule:/i), { target: { value: 'Action1' } });
             // Wait for the component to process the state update
             await waitFor(() => {
-                const inputFields = screen.getAllByLabelText(/Enter line number:/i);
+                const inputFields = screen.getAllByLabelText(/Line number:/i);
                 expect(inputFields.length).toBe(2);
             })
         });
 
         await act(async () => {
-            const inputs = screen.getAllByLabelText(/Enter line number:/i);
+            const inputs = screen.getAllByLabelText(/Line number:/i);
             fireEvent.change(inputs[0], { target: { value: '1' } });
 
             // Wait for the component to process the state update
@@ -133,7 +132,7 @@ describe('Menu Component', () => {
             })
         });
         await act(async () => {
-            const inputs = screen.getAllByLabelText(/Enter line number:/i);
+            const inputs = screen.getAllByLabelText(/Line number:/i);
             fireEvent.change(inputs[1], { target: { value: '2' } });
 
             // Wait for the component to process the state update
@@ -141,7 +140,7 @@ describe('Menu Component', () => {
                 expect((inputs[1] as HTMLInputElement).value).toBe('2');
             });
         });
-        const performButton = screen.getByRole('button', { name: /Perform Action/i });
+        const performButton = screen.getByRole('button', { name: /Apply Rule/i });
         fireEvent.click(performButton);
 
         await waitFor(() => {
@@ -179,12 +178,12 @@ describe('Menu Component', () => {
         fireEvent.change(screen.getByLabelText(/Select Inference Rule:/i), { target: { value: 'Action1' } });
 
         await waitFor(() => {
-            const inputs = screen.getAllByLabelText(/Enter line number:/i);
+            const inputs = screen.getAllByLabelText(/Line number:/i);
             fireEvent.change(inputs[0], { target: { value: '1' } });
             fireEvent.change(inputs[1], { target: { value: '2' } });
         });
 
-        const performButton = screen.getByRole('button', { name: /Perform Action/i });
+        const performButton = screen.getByRole('button', { name: /Apply Rule/i });
         fireEvent.click(performButton);
 
         await waitFor(() => {
@@ -199,7 +198,7 @@ describe('Menu Component', () => {
                 expect.any(Function)
             );
             expect(defaultProps.setProof).not.toHaveBeenCalled();
-            expect(window.alert).toHaveBeenCalledWith('Action failed: An error occurred');
+            expect(screen.getByRole('alert')).toHaveTextContent('An error occurred');
         });
     });
 });
diff --git a/frontend/src/components/modal/NewProofModal.css b/frontend/src/components/modal/NewProofModal.css
index 12c8c0770..47feac35b 100644
--- a/frontend/src/components/modal/NewProofModal.css
+++ b/frontend/src/components/modal/NewProofModal.css
@@ -1,93 +1,148 @@
-/* Modal Styles */
+/* Modal Overlay */
 .modal {
-    position: fixed;
-    top: 0;
-    left: 0;
-    width: 100%;
-    height: 100%;
-    background-color: rgba(0, 0, 0, 0.5); /* Semi-transparent background */
-    display: flex;
-    justify-content: center;
-    align-items: center;
-    z-index: 1000;
-  }
-  
-  .modal-content {
-    background-color: #fff;
-    padding: 20px;
-    border-radius: 8px;
-    width: 90%;
-    max-width: 500px;
-    box-shadow: 0 4px 8px rgba(0, 0, 0, 0.2);
-    text-align: center;
-  }
-  
-  .modal h2 {
-    margin-bottom: 20px;
-  }
-  
-  .modal-body {
-    margin-bottom: 20px;
-  }
-  
-  .modal-body label {
-    display: block;
-    margin-bottom: 8px;
-    font-weight: bold;
-  }
-  
-  .modal-body input {
-    width: calc(100% - 16px);
-    padding: 8px;
-    margin-bottom: 10px;
-    border-radius: 4px;
-    border: 1px solid #ccc;
-    font-size: 1rem;
-  }
-  
-  .add-premise-btn {
-    margin: 10px 0;
-    padding: 8px 12px;
-    font-size: 1rem;
-    border: none;
-    background-color: #007bff;
-    color: #fff;
-    border-radius: 4px;
-    cursor: pointer;
-  }
-  
-  .add-premise-btn:hover {
-    background-color: #0056b3;
-  }
-  
-  .modal-footer {
-    display: flex;
-    justify-content: space-between;
-  }
-  
-  .submit-btn, .close-btn {
-    padding: 8px 16px;
-    font-size: 1rem;
-    border: none;
-    border-radius: 4px;
-    cursor: pointer;
-  }
-  
-  .submit-btn {
-    background-color: #28a745;
-    color: #fff;
-  }
-  
-  .submit-btn:hover {
-    background-color: #218838;
-  }
-  
-  .close-btn {
-    background-color: #dc3545;
-    color: #fff;
-  }
-  
-  .close-btn:hover {
-    background-color: #c82333;
-  }
-  
\ No newline at end of file
+  position: fixed;
+  top: 0;
+  left: 0;
+  width: 100%;
+  height: 100%;
+  background-color: rgba(0, 0, 0, 0.5);
+  display: flex;
+  justify-content: center;
+  align-items: center;
+  z-index: 1000;
+}
+
+.modal-content {
+  background-color: #fff;
+  padding: 24px;
+  border-radius: 8px;
+  width: 90%;
+  max-width: 500px;
+  box-shadow: 0 4px 16px rgba(0, 0, 0, 0.25);
+  text-align: center;
+}
+
+.modal h2 {
+  margin: 0 0 20px 0;
+  font-size: 1.5rem;
+  color: #333;
+}
+
+.modal-body {
+  margin-bottom: 20px;
+  text-align: left;
+}
+
+.modal-section-label {
+  display: block;
+  margin-bottom: 8px;
+  font-weight: bold;
+  color: #333;
+}
+
+.premise-row {
+  display: flex;
+  align-items: center;
+  gap: 8px;
+  margin-bottom: 8px;
+}
+
+.premise-row input {
+  flex: 1;
+}
+
+.modal-body input {
+  width: 100%;
+  padding: 8px 10px;
+  margin-bottom: 0;
+  border-radius: 4px;
+  border: 1px solid #ccc;
+  font-size: 1rem;
+  box-sizing: border-box;
+  transition: border-color 0.2s;
+}
+
+.modal-body input:focus {
+  outline: none;
+  border-color: #007bff;
+  box-shadow: 0 0 0 3px rgba(0, 123, 255, 0.2);
+}
+
+.remove-premise-btn {
+  flex-shrink: 0;
+  width: 30px;
+  height: 30px;
+  padding: 0;
+  font-size: 1.2rem;
+  line-height: 1;
+  border: none;
+  background-color: #e0e0e0;
+  color: #555;
+  border-radius: 4px;
+  cursor: pointer;
+  display: flex;
+  align-items: center;
+  justify-content: center;
+}
+
+.remove-premise-btn:hover {
+  background-color: #dc3545;
+  color: #fff;
+}
+
+.add-premise-btn {
+  display: block;
+  margin: 8px 0 16px;
+  padding: 8px 12px;
+  font-size: 0.95rem;
+  border: 1px dashed #007bff;
+  background-color: transparent;
+  color: #007bff;
+  border-radius: 4px;
+  cursor: pointer;
+  transition: background-color 0.2s, color 0.2s;
+}
+
+.add-premise-btn:hover {
+  background-color: #007bff;
+  color: #fff;
+}
+
+.modal-footer {
+  display: flex;
+  justify-content: flex-end;
+  gap: 10px;
+}
+
+.submit-btn,
+.close-btn {
+  padding: 9px 18px;
+  font-size: 1rem;
+  border: none;
+  border-radius: 4px;
+  cursor: pointer;
+  transition: background-color 0.2s;
+}
+
+.submit-btn {
+  background-color: #28a745;
+  color: #fff;
+}
+
+.submit-btn:hover:not(:disabled) {
+  background-color: #218838;
+}
+
+.submit-btn:disabled {
+  background-color: #94d3a2;
+  cursor: not-allowed;
+}
+
+.close-btn {
+  background-color: #6c757d;
+  color: #fff;
+}
+
+.close-btn:hover {
+  background-color: #545b62;
+}
diff --git a/frontend/src/components/modal/NewProofModal.tsx b/frontend/src/components/modal/NewProofModal.tsx
index b00e43841..0cca53ce1 100644
--- a/frontend/src/components/modal/NewProofModal.tsx
+++ b/frontend/src/components/modal/NewProofModal.tsx
@@ -1,4 +1,4 @@
-import React, { FC, useState } from 'react';
+import React, { FC, useState, useEffect, useRef } from 'react';
 import './NewProofModal.css';
 
 type NewProofModalProps = {
@@ -10,8 +10,30 @@ type NewProofModalProps = {
 const NewProofModal: FC<NewProofModalProps> = ({ isOpen, onClose, onSubmit }) => {
   const [premises, setPremises] = useState<string[]>(['']);
   const [goal, setGoal] = useState('');
+  const firstInputRef = useRef<HTMLInputElement>(null);
+
+  // Close on Escape key
+  useEffect(() => {
+    if (!isOpen) return;
+    const handleKeyDown = (e: KeyboardEvent) => {
+      if (e.key === 'Escape') onClose();
+    };
+    document.addEventListener('keydown', handleKeyDown);
+    return () => document.removeEventListener('keydown', handleKeyDown);
+  }, [isOpen, onClose]);
+
+  // Focus first input when modal opens
+  useEffect(() => {
+    if (isOpen) {
+      setTimeout(() => firstInputRef.current?.focus(), 50);
+    }
+  }, [isOpen]);
 
   const handleAddPremise = () => setPremises([...premises, '']);
+  const handleRemovePremise = (index: number) => {
+    if (premises.length === 1) return;
+    setPremises(premises.filter((_, i) => i !== index));
+  };
   const handlePremiseChange = (index: number, value: string) => {
     const newPremises = [...premises];
     newPremises[index] = value;
@@ -27,38 +49,63 @@ const NewProofModal: FC<NewProofModalProps> = ({ isOpen, onClose, onSubmit }) =>
   if (!isOpen) return null;
 
   return (
-    <div className="modal">
+    <div
+      className="modal"
+      role="dialog"
+      aria-modal="true"
+      aria-labelledby="new-proof-modal-title"
+      onClick={(e) => { if (e.target === e.currentTarget) onClose(); }}
+    >
       <div className="modal-content">
-        <h2>New Proof</h2>
+        <h2 id="new-proof-modal-title">New Proof</h2>
         <div className="modal-body">
-          <label>Premises:</label>
+          <label className="modal-section-label">Premises:</label>
           {premises.map((premise, index) => (
-            <input
-              key={premise+index}
-              type="text"
-              value={premise}
-              onChange={(e) => handlePremiseChange(index, e.target.value)}
-              placeholder="Enter a premise"
-            />
+            <div key={index} className="premise-row">
+              <input
+                ref={index === 0 ? firstInputRef : undefined}
+                id={`premise-${index}`}
+                type="text"
+                value={premise}
+                onChange={(e) => handlePremiseChange(index, e.target.value)}
+                placeholder={`Premise ${index + 1}`}
+                aria-label={`Premise ${index + 1}`}
+              />
+              {premises.length > 1 && (
+                <button
+                  className="remove-premise-btn"
+                  onClick={() => handleRemovePremise(index)}
+                  aria-label={`Remove premise ${index + 1}`}
+                  title="Remove"
+                >
+                  ×
+                </button>
+              )}
+            </div>
           ))}
           <button className="add-premise-btn" onClick={handleAddPremise}>
             + Add Premise
           </button>
 
-          <label>Goal:</label>
+          <label htmlFor="modal-goal" className="modal-section-label">Goal:</label>
           <input
+            id="modal-goal"
             type="text"
             value={goal}
             onChange={(e) => handleGoalChange(e.target.value)}
-            placeholder="Enter the goal"
+            placeholder="Enter the goal expression"
           />
         </div>
         <div className="modal-footer">
-          <button className="submit-btn" onClick={handleSubmit}>
-            Submit
+          <button
+            className="submit-btn"
+            onClick={handleSubmit}
+            disabled={goal.trim() === ''}
+          >
+            Start Proof
           </button>
           <button className="close-btn" onClick={onClose}>
-            Close
+            Cancel
           </button>
         </div>
       </div>
diff --git a/frontend/src/components/modal/__test__/NewProofModal.test.tsx b/frontend/src/components/modal/__test__/NewProofModal.test.tsx
index e37849d0e..120d0748a 100644
--- a/frontend/src/components/modal/__test__/NewProofModal.test.tsx
+++ b/frontend/src/components/modal/__test__/NewProofModal.test.tsx
@@ -20,11 +20,11 @@ describe('NewProofModal Component', () => {
     const { getByText, getByPlaceholderText } = setup(true);
 
     expect(getByText('New Proof')).toBeInTheDocument();
-    expect(getByPlaceholderText('Enter a premise')).toBeInTheDocument();
-    expect(getByPlaceholderText('Enter the goal')).toBeInTheDocument();
+    expect(getByPlaceholderText('Premise 1')).toBeInTheDocument();
+    expect(getByPlaceholderText('Enter the goal expression')).toBeInTheDocument();
     expect(getByText('+ Add Premise')).toBeInTheDocument();
-    expect(getByText('Submit')).toBeInTheDocument();
-    expect(getByText('Close')).toBeInTheDocument();
+    expect(getByText('Start Proof')).toBeInTheDocument();
+    expect(getByText('Cancel')).toBeInTheDocument();
   });
 
   test('does not render when not open', () => {
@@ -34,30 +34,32 @@ describe('NewProofModal Component', () => {
   });
 
   test('can add a premise and update goal', () => {
-    const { getByText, getAllByPlaceholderText, getByPlaceholderText } = setup(true);
+    const { getByText, getByPlaceholderText } = setup(true);
 
     // Add a new premise
     fireEvent.click(getByText('+ Add Premise'));
-    const premiseInputs = getAllByPlaceholderText('Enter a premise');
-    expect(premiseInputs).toHaveLength(2);
+    const premise1 = getByPlaceholderText('Premise 1');
+    const premise2 = getByPlaceholderText('Premise 2');
+    expect(premise1).toBeInTheDocument();
+    expect(premise2).toBeInTheDocument();
 
     // Update premises and goal
-    fireEvent.change(premiseInputs[0], { target: { value: 'Premise 1' } });
-    fireEvent.change(premiseInputs[1], { target: { value: 'Premise 2' } });
-    fireEvent.change(getByPlaceholderText('Enter the goal'), { target: { value: 'Goal' } });
+    fireEvent.change(premise1, { target: { value: 'Premise 1 value' } });
+    fireEvent.change(premise2, { target: { value: 'Premise 2 value' } });
+    fireEvent.change(getByPlaceholderText('Enter the goal expression'), { target: { value: 'Goal' } });
 
-    expect((premiseInputs[0] as HTMLInputElement).value).toBe('Premise 1');
-    expect((premiseInputs[1] as HTMLInputElement).value).toBe('Premise 2');
-    expect((getByPlaceholderText('Enter the goal') as HTMLInputElement).value).toBe('Goal');
+    expect((premise1 as HTMLInputElement).value).toBe('Premise 1 value');
+    expect((premise2 as HTMLInputElement).value).toBe('Premise 2 value');
+    expect((getByPlaceholderText('Enter the goal expression') as HTMLInputElement).value).toBe('Goal');
   });
 
   test('submits correct data and closes modal', () => {
     const { getByText, getByPlaceholderText } = setup(true);
 
-    fireEvent.change(getByPlaceholderText('Enter a premise'), { target: { value: 'Premise 1' } });
-    fireEvent.change(getByPlaceholderText('Enter the goal'), { target: { value: 'Goal' } });
+    fireEvent.change(getByPlaceholderText('Premise 1'), { target: { value: 'Premise 1' } });
+    fireEvent.change(getByPlaceholderText('Enter the goal expression'), { target: { value: 'Goal' } });
 
-    fireEvent.click(getByText('Submit'));
+    fireEvent.click(getByText('Start Proof'));
 
     expect(onSubmitMock).toHaveBeenCalledWith(['Premise 1'], 'Goal');
     expect(onCloseMock).toHaveBeenCalled();
@@ -66,7 +68,7 @@ describe('NewProofModal Component', () => {
   test('closes modal without submitting when close button is clicked', () => {
     const { getByText } = setup(true);
 
-    fireEvent.click(getByText('Close'));
+    fireEvent.click(getByText('Cancel'));
 
     expect(onSubmitMock).not.toHaveBeenCalled();
     expect(onCloseMock).toHaveBeenCalled();
diff --git a/frontend/src/components/proof/ProofViewer.tsx b/frontend/src/components/proof/ProofViewer.tsx
index cc72e5bb0..c080ad2ef 100644
--- a/frontend/src/components/proof/ProofViewer.tsx
+++ b/frontend/src/components/proof/ProofViewer.tsx
@@ -26,21 +26,17 @@ export const ProofViewer: FC<ProofViewerProps> = ({ proof, coloring }) => {
     setHoveredRange(null);
   };
 
-  // Updated parseRangeFromRule to handle the general case with ranges and individual numbers
   const parseRangeFromRule = (rule: string): RangeDto[] | null => {
-    // Match all sequences inside the brackets
     let match = /\[(\d+(-\d+)?(, \d+(-\d+)?)*?)\]/.exec(rule);
     if (match) {
       const parts = match[1].split(',');
       let ranges: RangeDto[] = [];
 
       parts.forEach(part => {
-        // Check if the part is a range (e.g., "1-2")
         const rangeMatch = /(\d+)-(\d+)/.exec(part);
         if (rangeMatch) {
           ranges.push({ start: parseInt(rangeMatch[1]), end: parseInt(rangeMatch[2]) });
         } else {
-          // If it's not a range, treat it as a single number
           const number = parseInt(part);
           ranges.push({ start: number, end: number });
         }
@@ -59,22 +55,15 @@ export const ProofViewer: FC<ProofViewerProps> = ({ proof, coloring }) => {
   };
 
   return (
-    <div>
-      <hr
-        style={{
-          background: 'black',
-          color: 'black',
-          borderColor: 'black',
-          height: '3px',
-        }}
-      />
+    <div className="proof-viewer-wrapper">
+      <hr className="proof-divider" />
       <div className="proof-viewer">
-        <table>
+        <table aria-label="Proof steps">
           <thead>
             <tr>
-              <th>Line</th>
-              <th>Step</th>
-              <th>Rule</th>
+              <th scope="col">Line</th>
+              <th scope="col">Step</th>
+              <th scope="col">Rule</th>
             </tr>
           </thead>
           <tbody>
@@ -94,14 +83,7 @@ export const ProofViewer: FC<ProofViewerProps> = ({ proof, coloring }) => {
           </tbody>
         </table>
       </div>
-      <hr
-        style={{
-          background: 'black',
-          color: 'black',
-          borderColor: 'black',
-          height: '3px',
-        }}
-      />
+      <hr className="proof-divider" />
       <Goal
         expression={proof.goal}
         success={proof && proof.steps && proof.steps.length > 0 &&
diff --git a/frontend/src/service/actions.ts b/frontend/src/service/actions.ts
index 83ceb1c9b..bca75018e 100644
--- a/frontend/src/service/actions.ts
+++ b/frontend/src/service/actions.ts
@@ -18,5 +18,8 @@ export async function applyAction(logic: string, proof: ProofDto, action: Action
     })
         .then(response => response.text())
         .then(data => consumer(JSON.parse(data)))
-        .catch(err => console.error("Error applying an action:", err));
-}
\ No newline at end of file
+        .catch(err => {
+            console.error("Error applying an action:", err);
+            consumer({ success: false, message: 'Network error. Please try again.' });
+        });
+}