קובץ .dex הוא פורמט התעבורה של קוד באקס (bytecode) של Dalvik. יש אילוצים תחביריים וסמנטיים מסוימים שצריך לעמוד בהם כדי שקובץ יהיה קובץ .dex תקין, וסביבת זמן ריצה צריכה לתמוך רק בקובצי  .dex תקינים.
אילוצים כלליים על תקינות קובצי  .dex
אילוצים כלליים של תקינות קשורים למבנה הרחב יותר של קובץ .dex, כפי שמתואר בפירוט בפורמט .dex.
| מזהה | תיאור | 
|---|---|
| G1 | המספר magicבקובץ.dexצריך להיותdex\n035\0בגרסה 35, או מספר דומה בגרסאות מאוחרות יותר. | 
| G2 | סיכום הביקורת חייב להיות סיכום ביקורת Adler-32 של כל תוכן הקובץ, מלבד השדות magicו-checksum. | 
| G3 | החתימה חייבת להיות גיבוב SHA-1 של כל תוכן הקובץ, מלבד magic, checksumו-signature. | 
| G4 | השדה  השדה  | 
| G5 | הערך של  הערך של  | 
| G6 | הערך של endian_tagחייב להיות:ENDIAN_CONSTANTאוREVERSE_ENDIAN_CONSTANT | 
| G7 | בכל אחד מהקטעים  
            השדות  | 
| G8 | כל שדות ה-offset בכותרת, מלבד map_off, חייבים להיות מותאמים לארבעה בייטים. | 
| G9 | השדה map_offחייב להיות אפס או להפנות למקטע הנתונים. במקרה השני, המקטעdataחייב להתקיים. | 
| G10 | אסור שחלקים link, string_ids,type_ids, proto_ids, field_ids,method_ids, class_defsו-dataיחולו זה על זה או על הכותרת. | 
| G11 | אם המפה קיימת, לכל רשומה במפה צריך להיות סוג תקין. כל סוג יכול להופיע פעם אחת לכל היותר. | 
| G12 | אם המפה קיימת, לכל רשומה במפה צריכים להיות גודל וזזוג (offset) שאינם אפס. ההיסט חייב להצביע על הקטע המתאים בקובץ (כלומר, string_id_itemחייב להצביע על הקטעstring_ids) והגודל המפורש או המשתמע של הפריט חייב להתאים לתוכן ולגודל בפועל של הקטע. | 
| G13 | אם קיימת מפה, היסט הרשומה n+1במפה חייב להיות גדול מ-n plus than size of map entry nאו שווה לו. המשמעות היא שהרשאות לא חופפות והן מסודרות מערכים נמוכים לערכים גבוהים. | 
| G14 | לסוגים הבאים של רשומות צריך להיות אופלס שמותאם לארבע בייטים: string_id_item,type_id_item, proto_id_item,field_id_item,method_id_item, class_def_item,type_list, code_item,annotations_directory_item. | 
| G15 | לכל  לכל   בשדה  | 
| G16 | לכל type_id_item, השדהdescriptor_idxחייב להכיל הפניה תקפה לרשימהstring_ids. המחרוזת שצוינה צריכה להיות מתארת סוג תקינה. | 
| G17 | לכל proto_id_item, השדהshorty_idxחייב להכיל הפניה תקפה לרשימהstring_ids. המחרוזת שצוינה צריכה להיות מתארת של קיצור דרך תקינה. כמו כן, השדהreturn_type_idxחייב להיות אינדקס חוקי בקטעtype_ids, והשדהparameters_offחייב להיות אפס או שינוי אופסט חוקי שמפנה לקטעdata. אם הערך שונה מאפס, רשימת הפרמטרים לא יכולה לכלול רשומות ריקות. | 
| G18 | לכל field_id_item, השדותclass_idxו-type_idxחייבים להיות אינדקסים תקפים ברשימהtype_ids. הערך שמתייחס אליוclass_idxחייב להיות הפניה מסוג שאינו מערך. בנוסף, השדהname_idxחייב להיות הפניה תקינה לקטעstring_ids, ותוכן הרשומה שאליו מופנית ההפניה חייב לעמוד במפרטMemberName. | 
| G19 | לכל method_id_item, השדהclass_idxחייב להיות אינדקס חוקי למדורtype_ids, והרשומה שאליה מופנית ההפניה חייבת להיות מסוג הפניה שאינה מערך. השדהproto_idחייב להיות הפניה תקינה לרשימהproto_ids. השדהname_idxחייב להיות הפניה תקינה לקטעstring_ids, ותוכן הרשומה שאליו מופנית ההפניה חייב לעמוד במפרטMemberName. | 
| G20 | לכל field_id_item, השדהclass_idxחייב להיות אינדקס תקין ברשימהtype_ids. הרשומה שצוינה צריכה להיות מסוג הפניה שאינה מערך. | 
אילוצים של קוד בייט סטטי
אילוצים סטטיים הם אילוצים על רכיבים ספציפיים של קוד ה-bytecode. בדרך כלל אפשר לבדוק אותם בלי להשתמש בשיטות של בקרה או ניתוח תעבורת נתונים.
| מזהה | תיאור | 
|---|---|
| A1 | מערך insnsלא יכול להיות ריק. | 
| A2 | האינדקס של קוד הפקודה הראשון במערך insnsחייב להיות אפס. | 
| A3 | מערך insnsחייב להכיל רק קוד opcode תקף של Dalvik. | 
| A4 | האינדקס של ההוראה n+1חייב להיות שווה לאינדקס של ההוראהnבתוספת האורך של ההוראהn, תוך התחשבות באפשרויות של אופרנדים. | 
| A5 | ההוראה האחרונה במערך insnsחייבת להסתיים במדדinsns_size-1. | 
| A6 | כל היעדים של gotoו-if-<kind>חייבים להיות opcodes באותו method. | 
| A7 | כל היעדים של הוראה packed-switchחייבים להיות
          אופרקודים באותו method. הגודל והרשימה של היעדים חייבים להיות עקביים. | 
| A8 | כל היעדים של הוראה sparse-switchחייבים להיות
          אופרקודים באותו method. הטבלה התואמת חייבת להיות עקבית וממוינים מקטן לגדול. | 
| A9 | המשתנה Bשל ההוראותconst-stringו-const-string/jumboחייב להיות אינדקס תקין במאגר הקבועים של המחרוזות. | 
| A10 | המשתנה Cשל ההוראותiget<kind>ו-iput<kind>חייב להיות אינדקס תקין למאגר הקבועים של השדה. הרשומה שצוינה צריכה לייצג שדה של מכונה. | 
| A11 | המשתנה Cשל ההוראותsget<kind>ו-sput<kind>חייב להיות אינדקס תקין למאגר הקבועים של השדה. הרשומה שצוינה צריכה לייצג שדה סטטי. | 
| A12 | המשתנה Cשל ההוראותinvoke-virtual,invoke-super, invoke-directו-invoke-staticחייב להיות אינדקס תקין במאגר הקבועים של השיטה. | 
| A13 | המשתנה Bשל ההוראותinvoke-virtual/range,invoke-super/range,invoke-direct/rangeו-invoke-static/rangeחייב להיות אינדקס תקין במאגר הקבועים של השיטה. | 
| A14 | אפשר להפעיל שיטה ששמה מתחיל ב-'<' רק באופן סמלי על ידי המכונה הווירטואלית, ולא על ידי קוד שמקורו בקובץ .dex. החריג היחיד הוא ה-initializer של המופע, שאפשר להפעיל באמצעותinvoke-direct. | 
| A15 | המשתנה Cשל ההוראהinvoke-interfaceחייב להיות אינדקס תקין במאגר הקבועים של השיטה. המשתנהmethod_idשמצוין בהפניה חייב להיות שייך לממשק (ולא לכיתה). | 
| A16 | המשתנה Bשל ההוראהinvoke-interface/rangeחייב להיות אינדקס תקין במאגר הקבועים של השיטה.
          המשתנהmethod_idשמצוין בהפניה חייב להיות שייך לממשק (ולא לכיתה). | 
| A17 | המשתנה Bשל ההוראותconst-class,check-cast,new-instanceו-filled-new-array/rangeחייב להיות אינדקס תקף במאגר הקבועים של הסוגים. | 
| A18 | המשתנה Cשל ההוראותinstance-of,new-arrayו-filled-new-arrayחייב להיות אינדקס תקף במאגר הקבועים של הסוגים. | 
| A19 | המימדים של מערך שנוצר באמצעות הוראה new-arrayחייבים להיות קטנים מ-256. | 
| A20 | אסור להפנות את ההוראה newלממשקי, למחלקות מערך או למחלקות מופשטים. | 
| A21 | הסוג שאליו מפנה ההוראה new-arrayחייב להיות סוג חוקי שאינו סוג הפניה. | 
| A22 | כל הרשומות שמתייחסות להוראה ברוחב יחיד (לא זוג) חייבות להיות תקפות לשיטה הנוכחית. כלומר, האינדקסים שלהם חייבים להיות לא שליליים וקטנים מ- registers_size. | 
| A23 | כל הרשומות שמתייחסות להוראה בפורמט של רוחב כפול (זוג) חייבות להיות תקפות לשיטה הנוכחית. כלומר, האינדקסים שלהם חייבים להיות לא שליליים וקטנים מ- registers_size-1. | 
| A24 | המשתנה method_idשל ההוראותinvoke-virtualו-invoke-directחייב להיות שייך לכיתה (ולא לממשק). בקובצי Dex בגרסה037ואילך, התנאי הזה חייב להתקיים גם לגבי ההוראותinvoke-superו-invoke-static. | 
| A25 | המשתנה method_idשל ההוראותinvoke-virtual/rangeו-invoke-direct/rangeחייב להיות שייך לכיתה (ולא לממשק). בקובצי Dex בגרסה037ואילך, התנאי הזה חייב להתקיים גם לגבי ההוראותinvoke-super/rangeו-invoke-static/range. | 
מגבלות על קוד בייט מבני
אילוצים מבניים הם אילוצים על היחסים בין כמה רכיבים של הקוד. בדרך כלל אי אפשר לבדוק אותם בלי להשתמש בשיטות של בקרה או ניתוח תעבורת נתונים.
| מזהה | תיאור | 
|---|---|
| B1 | מספר הארגומנטים והסוגים שלהם (רישומים וערכים מיידיים) חייבים תמיד להתאים להוראה. | 
| B2 | אסור לפרק זוגות של רשומות. | 
| B3 | צריך להקצות רישום (או זוג) לפני שאפשר לקרוא אותו. | 
| B4 | הוראה invoke-directחייבת להפעיל מאתחלת של מופע או שיטה רק בכיתה הנוכחית או באחת מהסופר-כיתות שלה. | 
| B5 | צריך להפעיל את ה-initializer של המכונה רק במכונה שלא בוצע לה אתחול. | 
| B6 | אפשר להפעיל שיטות של מופעים רק במופעים שכבר הופעלו, וגישה לשדות של מופעים אפשרית רק במופעים שכבר הופעלו. | 
| B7 | אסור להשתמש ברשומה שמכילה את התוצאה של הוראה new-instanceאם אותה הוראהnew-instanceמופעלת שוב לפני שמפעילים את המכונה. | 
| B8 | מפעיל המכונה של המופע חייב לקרוא למפעיל מכונה אחר של מופע (מאותה כיתה או מאותה סופר-כיתה) לפני שאפשר לגשת למאפיינים של המופע.
           חריגים הם שדות של מופעים שלא עוברים בירושה, שאפשר להקצות
           לפני שמפעילים מערך נתונים אחר, והכיתה Objectבאופן כללי. | 
| B9 | כל הארגומנטים בפועל של השיטה חייבים להיות תואמים להקצאה לארגומנטים הפורמליים המתאימים שלהם. | 
| בּֽי 10 | בכל קריאה ל-method של מופע, המופע בפועל חייב להיות תואם להקצאה של הכיתה או הממשק שצוינו בהוראה. | 
| B11 | ההוראה return<kind>חייבת להתאים לסוג ההחזרה של השיטה. | 
| B12 | כשנכנסים למאפיינים מוגנים של סופר-קלאס, הסוג בפועל של המופע שאליו נכנסים חייב להיות הכיתה הנוכחית או אחת מהסופר-כיתות שלה. | 
| B13 | סוג הערך ששמור בשדה סטטי חייב להיות תואם להקצאה לסוג השדה או שניתן להמיר אותו לסוג השדה. | 
| B14 | סוג הערך ששמור בשדה חייב להיות תואם להקצאה לסוג השדה או שניתן להמיר אותו לסוג השדה. | 
| B15 | הסוג של כל ערך שנשמר במערך חייב להיות תואם למתן הערך לסוג הרכיב של המערך. | 
| B16 | המשתנה Aשל הוראהthrowחייב להיות תואם להקצאה שלjava.lang.Throwable. | 
| B17 | ההוראה האחרונה שאפשר להגיע אליה בשיטה חייבת להיות gotoאו הסתעפות לאחור,returnאוthrow. אסור להשאיר את מערךinsnsבתחתית. | 
| B18 | אי אפשר לקרוא את החלק שלא הוקצה של זוג רישום לשעבר (הוא נחשב לא חוקי) עד שהוא יוקצה מחדש באמצעות הוראה אחרת. | 
| B19 | לפני הוראת move-result<kind>חייבת להופיע הוראתinvoke-<kind>(באוסףinsns). היוצא מן הכלל היחיד הוא ההוראהmove-result-object, שיכולה גם להיות מקדימה לה הוראהfilled-new-array. | 
| B20 | לפני הוראה move-result<kind>חייבת להופיע (בזרימת הבקרה בפועל) הוראהreturn-<kind>תואמת (אסור לקפוץ אליה). היוצא מן הכלל היחיד הוא ההוראהmove-result-object, שיכולה גם להיות מקדימה לה הוראהfilled-new-array. | 
| B21 | הוראה move-exceptionחייבת להופיע רק כהוראה הראשונה בטיפול בחריגה. | 
| B22 | אסור שזרימת הבקרה תגיע לפקודות הפסאודו packed-switch-data,sparse-switch-dataו-fill-array-data. |